Left Termination of the query pattern
money(a,a,a,a,a,a,a,a)
w.r.t. the given Prolog program could successfully be proven:

0 Prolog
↳1 UnifyTransformerProof (⇔, 0 ms)
↳2 Prolog
↳3 UndefinedPredicateHandlerProof (⇒, 0 ms)
↳4 Prolog
↳5 PrologToPiTRSProof (⇒, 149 ms)
↳6 PiTRS
↳7 DependencyPairsProof (⇔, 618 ms)
↳8 PiDP
↳9 DependencyGraphProof (⇔, 0 ms)
↳10 AND
    ↳11 PiDP
        ↳12 UsableRulesProof (⇔, 0 ms)
        ↳13 PiDP
        ↳14 PiDPToQDPProof (⇒, 0 ms)
        ↳15 QDP
        ↳16 QDPSizeChangeProof (⇔, 0 ms)
        ↳17 YES
    ↳18 PiDP
        ↳19 UsableRulesProof (⇔, 0 ms)
        ↳20 PiDP
        ↳21 PiDPToQDPProof (⇒, 0 ms)
        ↳22 QDP
        ↳23 QDPSizeChangeProof (⇔, 0 ms)
        ↳24 YES

(0) Obligation:

Clauses:

demo :- ','(nl, ','(write('Cryptarithmetic puzzle'), ','(nl, ','(nl, ','(write(' SEND'), ','(nl, ','(write(' + MORE'), ','(nl, ','(write(' --------'), ','(nl, ','(write(' MONEY'), ','(nl, ','(nl, ','(nl, ','(time(X2), ','(money(S, E, N, D, M, O, R, Y), ','(time(T), ','(write('The solution is:'), ','(nl, ','(nl, ','(write(' '), ','(write(S), ','(write(E), ','(write(N), ','(write(D), ','(nl, ','(write(' + '), ','(write(M), ','(write(O), ','(write(R), ','(write(E), ','(nl, ','(write(' --------'), ','(nl, ','(write(' '), ','(write(M), ','(write(O), ','(write(N), ','(write(E), ','(write(Y), ','(nl, ','(nl, ','(write('Solved in '), ','(write(T), ','(write(' msec.'), nl))))))))))))))))))))))))))))))))))))))))))))).
time(0).
solve(.(S, .(E, .(N, .(D, .(M, .(O, .(R, .(Y, []))))))))) :- money(S, E, N, D, M, O, R, Y).
money(S, E, N, D, M, O, R, Y) :- ','(carry(C1), ','(carry(C2), ','(carry(C3), ','(carry(C4), ','(=(C4, M), ','(=\=(M, 0), ','(domain(.(S, .(E, .(N, .(D, .(M, .(O, .(R, .(Y, [])))))))), .(0, .(1, .(2, .(3, .(4, .(5, .(6, .(7, .(8, .(9, []))))))))))), ','(=\=(S, 0), ','(calc(C3, S, M, C4, O), ','(calc(C2, E, O, C3, N), ','(calc(C1, N, R, C2, E), calc(0, D, E, C1, Y)))))))))))).
calc(C0, D, E, C1, Y) :- ','(sum(C0, D, CD), ','(sum(CD, E, S), ','(carry10(C1, C10), sum(C10, Y, S)))).
sum(X, Y, Z) :- is(Z, +(X, Y)).
domain([], X3).
domain(.(X1, R), L) :- ','(del(X1, L, NL), domain(R, NL)).
del(X, .(X, T), T).
del(X, .(Y, T), .(Y, NT)) :- del(X, T, NT).
carry(1).
carry(0).
carry10(0, 0).
carry10(1, 10).

Query: money(a,a,a,a,a,a,a,a)

(1) UnifyTransformerProof (EQUIVALENT transformation)

Added a fact for the built-in = predicate [PROLOG].

(2) Obligation:

Clauses:

demo :- ','(nl, ','(write('Cryptarithmetic puzzle'), ','(nl, ','(nl, ','(write(' SEND'), ','(nl, ','(write(' + MORE'), ','(nl, ','(write(' --------'), ','(nl, ','(write(' MONEY'), ','(nl, ','(nl, ','(nl, ','(time(X2), ','(money(S, E, N, D, M, O, R, Y), ','(time(T), ','(write('The solution is:'), ','(nl, ','(nl, ','(write(' '), ','(write(S), ','(write(E), ','(write(N), ','(write(D), ','(nl, ','(write(' + '), ','(write(M), ','(write(O), ','(write(R), ','(write(E), ','(nl, ','(write(' --------'), ','(nl, ','(write(' '), ','(write(M), ','(write(O), ','(write(N), ','(write(E), ','(write(Y), ','(nl, ','(nl, ','(write('Solved in '), ','(write(T), ','(write(' msec.'), nl))))))))))))))))))))))))))))))))))))))))))))).
time(0).
solve(.(S, .(E, .(N, .(D, .(M, .(O, .(R, .(Y, []))))))))) :- money(S, E, N, D, M, O, R, Y).
money(S, E, N, D, M, O, R, Y) :- ','(carry(C1), ','(carry(C2), ','(carry(C3), ','(carry(C4), ','(=(C4, M), ','(=\=(M, 0), ','(domain(.(S, .(E, .(N, .(D, .(M, .(O, .(R, .(Y, [])))))))), .(0, .(1, .(2, .(3, .(4, .(5, .(6, .(7, .(8, .(9, []))))))))))), ','(=\=(S, 0), ','(calc(C3, S, M, C4, O), ','(calc(C2, E, O, C3, N), ','(calc(C1, N, R, C2, E), calc(0, D, E, C1, Y)))))))))))).
calc(C0, D, E, C1, Y) :- ','(sum(C0, D, CD), ','(sum(CD, E, S), ','(carry10(C1, C10), sum(C10, Y, S)))).
sum(X, Y, Z) :- is(Z, +(X, Y)).
domain([], X3).
domain(.(X1, R), L) :- ','(del(X1, L, NL), domain(R, NL)).
del(X, .(X, T), T).
del(X, .(Y, T), .(Y, NT)) :- del(X, T, NT).
carry(1).
carry(0).
carry10(0, 0).
carry10(1, 10).
=(X, X).

Query: money(a,a,a,a,a,a,a,a)

(3) UndefinedPredicateHandlerProof (SOUND transformation)

Added facts for all undefined predicates [PROLOG].

(4) Obligation:

Clauses:

demo :- ','(nl, ','(write('Cryptarithmetic puzzle'), ','(nl, ','(nl, ','(write(' SEND'), ','(nl, ','(write(' + MORE'), ','(nl, ','(write(' --------'), ','(nl, ','(write(' MONEY'), ','(nl, ','(nl, ','(nl, ','(time(X2), ','(money(S, E, N, D, M, O, R, Y), ','(time(T), ','(write('The solution is:'), ','(nl, ','(nl, ','(write(' '), ','(write(S), ','(write(E), ','(write(N), ','(write(D), ','(nl, ','(write(' + '), ','(write(M), ','(write(O), ','(write(R), ','(write(E), ','(nl, ','(write(' --------'), ','(nl, ','(write(' '), ','(write(M), ','(write(O), ','(write(N), ','(write(E), ','(write(Y), ','(nl, ','(nl, ','(write('Solved in '), ','(write(T), ','(write(' msec.'), nl))))))))))))))))))))))))))))))))))))))))))))).
time(0).
solve(.(S, .(E, .(N, .(D, .(M, .(O, .(R, .(Y, []))))))))) :- money(S, E, N, D, M, O, R, Y).
money(S, E, N, D, M, O, R, Y) :- ','(carry(C1), ','(carry(C2), ','(carry(C3), ','(carry(C4), ','(=(C4, M), ','(=\=(M, 0), ','(domain(.(S, .(E, .(N, .(D, .(M, .(O, .(R, .(Y, [])))))))), .(0, .(1, .(2, .(3, .(4, .(5, .(6, .(7, .(8, .(9, []))))))))))), ','(=\=(S, 0), ','(calc(C3, S, M, C4, O), ','(calc(C2, E, O, C3, N), ','(calc(C1, N, R, C2, E), calc(0, D, E, C1, Y)))))))))))).
calc(C0, D, E, C1, Y) :- ','(sum(C0, D, CD), ','(sum(CD, E, S), ','(carry10(C1, C10), sum(C10, Y, S)))).
sum(X, Y, Z) :- is(Z, +(X, Y)).
domain([], X3).
domain(.(X1, R), L) :- ','(del(X1, L, NL), domain(R, NL)).
del(X, .(X, T), T).
del(X, .(Y, T), .(Y, NT)) :- del(X, T, NT).
carry(1).
carry(0).
carry10(0, 0).
carry10(1, 10).
=(X, X).
nl.
write(X0).
=\=(X0, X1).
is(X0, X1).

Query: money(a,a,a,a,a,a,a,a)

(5) PrologToPiTRSProof (SOUND transformation)

We use the technique of [TOCL09]. With regard to the inferred argument filtering the predicates were used in the following modes:
money_in: (f,f,f,f,f,f,f,f)
domain_in: (b,b)
del_in: (f,b,f)
calc_in: (b,f,b,b,f) (b,f,f,b,f)
sum_in: (b,f,f) (f,b,f) (f,f,f)
Transforming Prolog into the following Term Rewriting System:
Pi-finite rewrite system:
The TRS R consists of the following rules:

money_in_aaaaaaaa(S, E, N, D, M, O, R, Y) → U48_aaaaaaaa(S, E, N, D, M, O, R, Y, carry_in_a(C1))
carry_in_a(1) → carry_out_a(1)
carry_in_a(0) → carry_out_a(0)
U48_aaaaaaaa(S, E, N, D, M, O, R, Y, carry_out_a(C1)) → U49_aaaaaaaa(S, E, N, D, M, O, R, Y, C1, carry_in_a(C2))
U49_aaaaaaaa(S, E, N, D, M, O, R, Y, C1, carry_out_a(C2)) → U50_aaaaaaaa(S, E, N, D, M, O, R, Y, C1, C2, carry_in_a(C3))
U50_aaaaaaaa(S, E, N, D, M, O, R, Y, C1, C2, carry_out_a(C3)) → U51_aaaaaaaa(S, E, N, D, M, O, R, Y, C1, C2, C3, carry_in_a(C4))
U51_aaaaaaaa(S, E, N, D, M, O, R, Y, C1, C2, C3, carry_out_a(C4)) → U52_aaaaaaaa(S, E, N, D, M, O, R, Y, C1, C2, C3, C4, =_in_ga(C4, M))
=_in_ga(X, X) → =_out_ga(X, X)
U52_aaaaaaaa(S, E, N, D, M, O, R, Y, C1, C2, C3, C4, =_out_ga(C4, M)) → U53_aaaaaaaa(S, E, N, D, M, O, R, Y, C1, C2, C3, C4, =\=_in_gg(M, 0))
=\=_in_gg(X0, X1) → =\=_out_gg(X0, X1)
U53_aaaaaaaa(S, E, N, D, M, O, R, Y, C1, C2, C3, C4, =\=_out_gg(M, 0)) → U54_aaaaaaaa(S, E, N, D, M, O, R, Y, C1, C2, C3, C4, domain_in_gg(.(S, .(E, .(N, .(D, .(M, .(O, .(R, .(Y, [])))))))), .(0, .(1, .(2, .(3, .(4, .(5, .(6, .(7, .(8, .(9, []))))))))))))
domain_in_gg([], X3) → domain_out_gg([], X3)
domain_in_gg(.(X1, R), L) → U65_gg(X1, R, L, del_in_aga(X1, L, NL))
del_in_aga(X, .(X, T), T) → del_out_aga(X, .(X, T), T)
del_in_aga(X, .(Y, T), .(Y, NT)) → U67_aga(X, Y, T, NT, del_in_aga(X, T, NT))
U67_aga(X, Y, T, NT, del_out_aga(X, T, NT)) → del_out_aga(X, .(Y, T), .(Y, NT))
U65_gg(X1, R, L, del_out_aga(X1, L, NL)) → U66_gg(X1, R, L, domain_in_gg(R, NL))
U66_gg(X1, R, L, domain_out_gg(R, NL)) → domain_out_gg(.(X1, R), L)
U54_aaaaaaaa(S, E, N, D, M, O, R, Y, C1, C2, C3, C4, domain_out_gg(.(S, .(E, .(N, .(D, .(M, .(O, .(R, .(Y, [])))))))), .(0, .(1, .(2, .(3, .(4, .(5, .(6, .(7, .(8, .(9, [])))))))))))) → U55_aaaaaaaa(S, E, N, D, M, O, R, Y, C1, C2, C3, C4, =\=_in_ag(S, 0))
=\=_in_ag(X0, X1) → =\=_out_ag(X0, X1)
U55_aaaaaaaa(S, E, N, D, M, O, R, Y, C1, C2, C3, C4, =\=_out_ag(S, 0)) → U56_aaaaaaaa(S, E, N, D, M, O, R, Y, C1, C2, C3, calc_in_gagga(C3, S, M, C4, O))
calc_in_gagga(C0, D, E, C1, Y) → U60_gagga(C0, D, E, C1, Y, sum_in_gaa(C0, D, CD))
sum_in_gaa(X, Y, Z) → U64_gaa(X, Y, Z, is_in_ag(Z, +(X, Y)))
is_in_ag(X0, X1) → is_out_ag(X0, X1)
U64_gaa(X, Y, Z, is_out_ag(Z, +(X, Y))) → sum_out_gaa(X, Y, Z)
U60_gagga(C0, D, E, C1, Y, sum_out_gaa(C0, D, CD)) → U61_gagga(C0, D, E, C1, Y, sum_in_aga(CD, E, S))
sum_in_aga(X, Y, Z) → U64_aga(X, Y, Z, is_in_ag(Z, +(X, Y)))
U64_aga(X, Y, Z, is_out_ag(Z, +(X, Y))) → sum_out_aga(X, Y, Z)
U61_gagga(C0, D, E, C1, Y, sum_out_aga(CD, E, S)) → U62_gagga(C0, D, E, C1, Y, S, carry10_in_ga(C1, C10))
carry10_in_ga(0, 0) → carry10_out_ga(0, 0)
carry10_in_ga(1, 10) → carry10_out_ga(1, 10)
U62_gagga(C0, D, E, C1, Y, S, carry10_out_ga(C1, C10)) → U63_gagga(C0, D, E, C1, Y, sum_in_gaa(C10, Y, S))
U63_gagga(C0, D, E, C1, Y, sum_out_gaa(C10, Y, S)) → calc_out_gagga(C0, D, E, C1, Y)
U56_aaaaaaaa(S, E, N, D, M, O, R, Y, C1, C2, C3, calc_out_gagga(C3, S, M, C4, O)) → U57_aaaaaaaa(S, E, N, D, M, O, R, Y, C1, C2, calc_in_gaaga(C2, E, O, C3, N))
calc_in_gaaga(C0, D, E, C1, Y) → U60_gaaga(C0, D, E, C1, Y, sum_in_gaa(C0, D, CD))
U60_gaaga(C0, D, E, C1, Y, sum_out_gaa(C0, D, CD)) → U61_gaaga(C0, D, E, C1, Y, sum_in_aaa(CD, E, S))
sum_in_aaa(X, Y, Z) → U64_aaa(X, Y, Z, is_in_ag(Z, +(X, Y)))
U64_aaa(X, Y, Z, is_out_ag(Z, +(X, Y))) → sum_out_aaa(X, Y, Z)
U61_gaaga(C0, D, E, C1, Y, sum_out_aaa(CD, E, S)) → U62_gaaga(C0, D, E, C1, Y, S, carry10_in_ga(C1, C10))
U62_gaaga(C0, D, E, C1, Y, S, carry10_out_ga(C1, C10)) → U63_gaaga(C0, D, E, C1, Y, sum_in_gaa(C10, Y, S))
U63_gaaga(C0, D, E, C1, Y, sum_out_gaa(C10, Y, S)) → calc_out_gaaga(C0, D, E, C1, Y)
U57_aaaaaaaa(S, E, N, D, M, O, R, Y, C1, C2, calc_out_gaaga(C2, E, O, C3, N)) → U58_aaaaaaaa(S, E, N, D, M, O, R, Y, C1, calc_in_gaaga(C1, N, R, C2, E))
U58_aaaaaaaa(S, E, N, D, M, O, R, Y, C1, calc_out_gaaga(C1, N, R, C2, E)) → U59_aaaaaaaa(S, E, N, D, M, O, R, Y, calc_in_gaaga(0, D, E, C1, Y))
U59_aaaaaaaa(S, E, N, D, M, O, R, Y, calc_out_gaaga(0, D, E, C1, Y)) → money_out_aaaaaaaa(S, E, N, D, M, O, R, Y)

The argument filtering Pi contains the following mapping:
money_in_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8)  =  money_in_aaaaaaaa
U48_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U48_aaaaaaaa(x9)
carry_in_a(x1)  =  carry_in_a
carry_out_a(x1)  =  carry_out_a(x1)
U49_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)  =  U49_aaaaaaaa(x9, x10)
U50_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11)  =  U50_aaaaaaaa(x9, x10, x11)
U51_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12)  =  U51_aaaaaaaa(x9, x10, x11, x12)
U52_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13)  =  U52_aaaaaaaa(x9, x10, x11, x12, x13)
=_in_ga(x1, x2)  =  =_in_ga(x1)
=_out_ga(x1, x2)  =  =_out_ga(x2)
U53_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13)  =  U53_aaaaaaaa(x5, x9, x10, x11, x12, x13)
=\=_in_gg(x1, x2)  =  =\=_in_gg(x1, x2)
=\=_out_gg(x1, x2)  =  =\=_out_gg
0  =  0
U54_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13)  =  U54_aaaaaaaa(x5, x9, x10, x11, x12, x13)
domain_in_gg(x1, x2)  =  domain_in_gg(x1, x2)
.(x1, x2)  =  .(x2)
[]  =  []
domain_out_gg(x1, x2)  =  domain_out_gg
U65_gg(x1, x2, x3, x4)  =  U65_gg(x2, x4)
del_in_aga(x1, x2, x3)  =  del_in_aga(x2)
del_out_aga(x1, x2, x3)  =  del_out_aga(x3)
U67_aga(x1, x2, x3, x4, x5)  =  U67_aga(x5)
U66_gg(x1, x2, x3, x4)  =  U66_gg(x4)
U55_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13)  =  U55_aaaaaaaa(x5, x9, x10, x11, x12, x13)
=\=_in_ag(x1, x2)  =  =\=_in_ag(x2)
=\=_out_ag(x1, x2)  =  =\=_out_ag
U56_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12)  =  U56_aaaaaaaa(x5, x9, x10, x11, x12)
calc_in_gagga(x1, x2, x3, x4, x5)  =  calc_in_gagga(x1, x3, x4)
U60_gagga(x1, x2, x3, x4, x5, x6)  =  U60_gagga(x3, x4, x6)
sum_in_gaa(x1, x2, x3)  =  sum_in_gaa(x1)
U64_gaa(x1, x2, x3, x4)  =  U64_gaa(x4)
is_in_ag(x1, x2)  =  is_in_ag(x2)
+(x1, x2)  =  +
is_out_ag(x1, x2)  =  is_out_ag
sum_out_gaa(x1, x2, x3)  =  sum_out_gaa
U61_gagga(x1, x2, x3, x4, x5, x6)  =  U61_gagga(x4, x6)
sum_in_aga(x1, x2, x3)  =  sum_in_aga(x2)
U64_aga(x1, x2, x3, x4)  =  U64_aga(x4)
sum_out_aga(x1, x2, x3)  =  sum_out_aga
U62_gagga(x1, x2, x3, x4, x5, x6, x7)  =  U62_gagga(x7)
carry10_in_ga(x1, x2)  =  carry10_in_ga(x1)
carry10_out_ga(x1, x2)  =  carry10_out_ga(x2)
1  =  1
U63_gagga(x1, x2, x3, x4, x5, x6)  =  U63_gagga(x6)
calc_out_gagga(x1, x2, x3, x4, x5)  =  calc_out_gagga
U57_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11)  =  U57_aaaaaaaa(x5, x9, x10, x11)
calc_in_gaaga(x1, x2, x3, x4, x5)  =  calc_in_gaaga(x1, x4)
U60_gaaga(x1, x2, x3, x4, x5, x6)  =  U60_gaaga(x4, x6)
U61_gaaga(x1, x2, x3, x4, x5, x6)  =  U61_gaaga(x4, x6)
sum_in_aaa(x1, x2, x3)  =  sum_in_aaa
U64_aaa(x1, x2, x3, x4)  =  U64_aaa(x4)
sum_out_aaa(x1, x2, x3)  =  sum_out_aaa
U62_gaaga(x1, x2, x3, x4, x5, x6, x7)  =  U62_gaaga(x7)
U63_gaaga(x1, x2, x3, x4, x5, x6)  =  U63_gaaga(x6)
calc_out_gaaga(x1, x2, x3, x4, x5)  =  calc_out_gaaga
U58_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)  =  U58_aaaaaaaa(x5, x9, x10)
U59_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U59_aaaaaaaa(x5, x9)
money_out_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8)  =  money_out_aaaaaaaa(x5)

Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog

(6) Obligation:

Pi-finite rewrite system:
The TRS R consists of the following rules:

money_in_aaaaaaaa(S, E, N, D, M, O, R, Y) → U48_aaaaaaaa(S, E, N, D, M, O, R, Y, carry_in_a(C1))
carry_in_a(1) → carry_out_a(1)
carry_in_a(0) → carry_out_a(0)
U48_aaaaaaaa(S, E, N, D, M, O, R, Y, carry_out_a(C1)) → U49_aaaaaaaa(S, E, N, D, M, O, R, Y, C1, carry_in_a(C2))
U49_aaaaaaaa(S, E, N, D, M, O, R, Y, C1, carry_out_a(C2)) → U50_aaaaaaaa(S, E, N, D, M, O, R, Y, C1, C2, carry_in_a(C3))
U50_aaaaaaaa(S, E, N, D, M, O, R, Y, C1, C2, carry_out_a(C3)) → U51_aaaaaaaa(S, E, N, D, M, O, R, Y, C1, C2, C3, carry_in_a(C4))
U51_aaaaaaaa(S, E, N, D, M, O, R, Y, C1, C2, C3, carry_out_a(C4)) → U52_aaaaaaaa(S, E, N, D, M, O, R, Y, C1, C2, C3, C4, =_in_ga(C4, M))
=_in_ga(X, X) → =_out_ga(X, X)
U52_aaaaaaaa(S, E, N, D, M, O, R, Y, C1, C2, C3, C4, =_out_ga(C4, M)) → U53_aaaaaaaa(S, E, N, D, M, O, R, Y, C1, C2, C3, C4, =\=_in_gg(M, 0))
=\=_in_gg(X0, X1) → =\=_out_gg(X0, X1)
U53_aaaaaaaa(S, E, N, D, M, O, R, Y, C1, C2, C3, C4, =\=_out_gg(M, 0)) → U54_aaaaaaaa(S, E, N, D, M, O, R, Y, C1, C2, C3, C4, domain_in_gg(.(S, .(E, .(N, .(D, .(M, .(O, .(R, .(Y, [])))))))), .(0, .(1, .(2, .(3, .(4, .(5, .(6, .(7, .(8, .(9, []))))))))))))
domain_in_gg([], X3) → domain_out_gg([], X3)
domain_in_gg(.(X1, R), L) → U65_gg(X1, R, L, del_in_aga(X1, L, NL))
del_in_aga(X, .(X, T), T) → del_out_aga(X, .(X, T), T)
del_in_aga(X, .(Y, T), .(Y, NT)) → U67_aga(X, Y, T, NT, del_in_aga(X, T, NT))
U67_aga(X, Y, T, NT, del_out_aga(X, T, NT)) → del_out_aga(X, .(Y, T), .(Y, NT))
U65_gg(X1, R, L, del_out_aga(X1, L, NL)) → U66_gg(X1, R, L, domain_in_gg(R, NL))
U66_gg(X1, R, L, domain_out_gg(R, NL)) → domain_out_gg(.(X1, R), L)
U54_aaaaaaaa(S, E, N, D, M, O, R, Y, C1, C2, C3, C4, domain_out_gg(.(S, .(E, .(N, .(D, .(M, .(O, .(R, .(Y, [])))))))), .(0, .(1, .(2, .(3, .(4, .(5, .(6, .(7, .(8, .(9, [])))))))))))) → U55_aaaaaaaa(S, E, N, D, M, O, R, Y, C1, C2, C3, C4, =\=_in_ag(S, 0))
=\=_in_ag(X0, X1) → =\=_out_ag(X0, X1)
U55_aaaaaaaa(S, E, N, D, M, O, R, Y, C1, C2, C3, C4, =\=_out_ag(S, 0)) → U56_aaaaaaaa(S, E, N, D, M, O, R, Y, C1, C2, C3, calc_in_gagga(C3, S, M, C4, O))
calc_in_gagga(C0, D, E, C1, Y) → U60_gagga(C0, D, E, C1, Y, sum_in_gaa(C0, D, CD))
sum_in_gaa(X, Y, Z) → U64_gaa(X, Y, Z, is_in_ag(Z, +(X, Y)))
is_in_ag(X0, X1) → is_out_ag(X0, X1)
U64_gaa(X, Y, Z, is_out_ag(Z, +(X, Y))) → sum_out_gaa(X, Y, Z)
U60_gagga(C0, D, E, C1, Y, sum_out_gaa(C0, D, CD)) → U61_gagga(C0, D, E, C1, Y, sum_in_aga(CD, E, S))
sum_in_aga(X, Y, Z) → U64_aga(X, Y, Z, is_in_ag(Z, +(X, Y)))
U64_aga(X, Y, Z, is_out_ag(Z, +(X, Y))) → sum_out_aga(X, Y, Z)
U61_gagga(C0, D, E, C1, Y, sum_out_aga(CD, E, S)) → U62_gagga(C0, D, E, C1, Y, S, carry10_in_ga(C1, C10))
carry10_in_ga(0, 0) → carry10_out_ga(0, 0)
carry10_in_ga(1, 10) → carry10_out_ga(1, 10)
U62_gagga(C0, D, E, C1, Y, S, carry10_out_ga(C1, C10)) → U63_gagga(C0, D, E, C1, Y, sum_in_gaa(C10, Y, S))
U63_gagga(C0, D, E, C1, Y, sum_out_gaa(C10, Y, S)) → calc_out_gagga(C0, D, E, C1, Y)
U56_aaaaaaaa(S, E, N, D, M, O, R, Y, C1, C2, C3, calc_out_gagga(C3, S, M, C4, O)) → U57_aaaaaaaa(S, E, N, D, M, O, R, Y, C1, C2, calc_in_gaaga(C2, E, O, C3, N))
calc_in_gaaga(C0, D, E, C1, Y) → U60_gaaga(C0, D, E, C1, Y, sum_in_gaa(C0, D, CD))
U60_gaaga(C0, D, E, C1, Y, sum_out_gaa(C0, D, CD)) → U61_gaaga(C0, D, E, C1, Y, sum_in_aaa(CD, E, S))
sum_in_aaa(X, Y, Z) → U64_aaa(X, Y, Z, is_in_ag(Z, +(X, Y)))
U64_aaa(X, Y, Z, is_out_ag(Z, +(X, Y))) → sum_out_aaa(X, Y, Z)
U61_gaaga(C0, D, E, C1, Y, sum_out_aaa(CD, E, S)) → U62_gaaga(C0, D, E, C1, Y, S, carry10_in_ga(C1, C10))
U62_gaaga(C0, D, E, C1, Y, S, carry10_out_ga(C1, C10)) → U63_gaaga(C0, D, E, C1, Y, sum_in_gaa(C10, Y, S))
U63_gaaga(C0, D, E, C1, Y, sum_out_gaa(C10, Y, S)) → calc_out_gaaga(C0, D, E, C1, Y)
U57_aaaaaaaa(S, E, N, D, M, O, R, Y, C1, C2, calc_out_gaaga(C2, E, O, C3, N)) → U58_aaaaaaaa(S, E, N, D, M, O, R, Y, C1, calc_in_gaaga(C1, N, R, C2, E))
U58_aaaaaaaa(S, E, N, D, M, O, R, Y, C1, calc_out_gaaga(C1, N, R, C2, E)) → U59_aaaaaaaa(S, E, N, D, M, O, R, Y, calc_in_gaaga(0, D, E, C1, Y))
U59_aaaaaaaa(S, E, N, D, M, O, R, Y, calc_out_gaaga(0, D, E, C1, Y)) → money_out_aaaaaaaa(S, E, N, D, M, O, R, Y)

The argument filtering Pi contains the following mapping:
money_in_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8)  =  money_in_aaaaaaaa
U48_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U48_aaaaaaaa(x9)
carry_in_a(x1)  =  carry_in_a
carry_out_a(x1)  =  carry_out_a(x1)
U49_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)  =  U49_aaaaaaaa(x9, x10)
U50_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11)  =  U50_aaaaaaaa(x9, x10, x11)
U51_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12)  =  U51_aaaaaaaa(x9, x10, x11, x12)
U52_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13)  =  U52_aaaaaaaa(x9, x10, x11, x12, x13)
=_in_ga(x1, x2)  =  =_in_ga(x1)
=_out_ga(x1, x2)  =  =_out_ga(x2)
U53_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13)  =  U53_aaaaaaaa(x5, x9, x10, x11, x12, x13)
=\=_in_gg(x1, x2)  =  =\=_in_gg(x1, x2)
=\=_out_gg(x1, x2)  =  =\=_out_gg
0  =  0
U54_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13)  =  U54_aaaaaaaa(x5, x9, x10, x11, x12, x13)
domain_in_gg(x1, x2)  =  domain_in_gg(x1, x2)
.(x1, x2)  =  .(x2)
[]  =  []
domain_out_gg(x1, x2)  =  domain_out_gg
U65_gg(x1, x2, x3, x4)  =  U65_gg(x2, x4)
del_in_aga(x1, x2, x3)  =  del_in_aga(x2)
del_out_aga(x1, x2, x3)  =  del_out_aga(x3)
U67_aga(x1, x2, x3, x4, x5)  =  U67_aga(x5)
U66_gg(x1, x2, x3, x4)  =  U66_gg(x4)
U55_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13)  =  U55_aaaaaaaa(x5, x9, x10, x11, x12, x13)
=\=_in_ag(x1, x2)  =  =\=_in_ag(x2)
=\=_out_ag(x1, x2)  =  =\=_out_ag
U56_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12)  =  U56_aaaaaaaa(x5, x9, x10, x11, x12)
calc_in_gagga(x1, x2, x3, x4, x5)  =  calc_in_gagga(x1, x3, x4)
U60_gagga(x1, x2, x3, x4, x5, x6)  =  U60_gagga(x3, x4, x6)
sum_in_gaa(x1, x2, x3)  =  sum_in_gaa(x1)
U64_gaa(x1, x2, x3, x4)  =  U64_gaa(x4)
is_in_ag(x1, x2)  =  is_in_ag(x2)
+(x1, x2)  =  +
is_out_ag(x1, x2)  =  is_out_ag
sum_out_gaa(x1, x2, x3)  =  sum_out_gaa
U61_gagga(x1, x2, x3, x4, x5, x6)  =  U61_gagga(x4, x6)
sum_in_aga(x1, x2, x3)  =  sum_in_aga(x2)
U64_aga(x1, x2, x3, x4)  =  U64_aga(x4)
sum_out_aga(x1, x2, x3)  =  sum_out_aga
U62_gagga(x1, x2, x3, x4, x5, x6, x7)  =  U62_gagga(x7)
carry10_in_ga(x1, x2)  =  carry10_in_ga(x1)
carry10_out_ga(x1, x2)  =  carry10_out_ga(x2)
1  =  1
U63_gagga(x1, x2, x3, x4, x5, x6)  =  U63_gagga(x6)
calc_out_gagga(x1, x2, x3, x4, x5)  =  calc_out_gagga
U57_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11)  =  U57_aaaaaaaa(x5, x9, x10, x11)
calc_in_gaaga(x1, x2, x3, x4, x5)  =  calc_in_gaaga(x1, x4)
U60_gaaga(x1, x2, x3, x4, x5, x6)  =  U60_gaaga(x4, x6)
U61_gaaga(x1, x2, x3, x4, x5, x6)  =  U61_gaaga(x4, x6)
sum_in_aaa(x1, x2, x3)  =  sum_in_aaa
U64_aaa(x1, x2, x3, x4)  =  U64_aaa(x4)
sum_out_aaa(x1, x2, x3)  =  sum_out_aaa
U62_gaaga(x1, x2, x3, x4, x5, x6, x7)  =  U62_gaaga(x7)
U63_gaaga(x1, x2, x3, x4, x5, x6)  =  U63_gaaga(x6)
calc_out_gaaga(x1, x2, x3, x4, x5)  =  calc_out_gaaga
U58_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)  =  U58_aaaaaaaa(x5, x9, x10)
U59_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U59_aaaaaaaa(x5, x9)
money_out_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8)  =  money_out_aaaaaaaa(x5)

(7) DependencyPairsProof (EQUIVALENT transformation)

Using Dependency Pairs [AG00,LOPSTR] we result in the following initial DP problem:
Pi DP problem:
The TRS P consists of the following rules:

MONEY_IN_AAAAAAAA(S, E, N, D, M, O, R, Y) → U48_AAAAAAAA(S, E, N, D, M, O, R, Y, carry_in_a(C1))
MONEY_IN_AAAAAAAA(S, E, N, D, M, O, R, Y) → CARRY_IN_A(C1)
U48_AAAAAAAA(S, E, N, D, M, O, R, Y, carry_out_a(C1)) → U49_AAAAAAAA(S, E, N, D, M, O, R, Y, C1, carry_in_a(C2))
U48_AAAAAAAA(S, E, N, D, M, O, R, Y, carry_out_a(C1)) → CARRY_IN_A(C2)
U49_AAAAAAAA(S, E, N, D, M, O, R, Y, C1, carry_out_a(C2)) → U50_AAAAAAAA(S, E, N, D, M, O, R, Y, C1, C2, carry_in_a(C3))
U49_AAAAAAAA(S, E, N, D, M, O, R, Y, C1, carry_out_a(C2)) → CARRY_IN_A(C3)
U50_AAAAAAAA(S, E, N, D, M, O, R, Y, C1, C2, carry_out_a(C3)) → U51_AAAAAAAA(S, E, N, D, M, O, R, Y, C1, C2, C3, carry_in_a(C4))
U50_AAAAAAAA(S, E, N, D, M, O, R, Y, C1, C2, carry_out_a(C3)) → CARRY_IN_A(C4)
U51_AAAAAAAA(S, E, N, D, M, O, R, Y, C1, C2, C3, carry_out_a(C4)) → U52_AAAAAAAA(S, E, N, D, M, O, R, Y, C1, C2, C3, C4, =_in_ga(C4, M))
U51_AAAAAAAA(S, E, N, D, M, O, R, Y, C1, C2, C3, carry_out_a(C4)) → =_IN_GA(C4, M)
U52_AAAAAAAA(S, E, N, D, M, O, R, Y, C1, C2, C3, C4, =_out_ga(C4, M)) → U53_AAAAAAAA(S, E, N, D, M, O, R, Y, C1, C2, C3, C4, =\=_in_gg(M, 0))
U52_AAAAAAAA(S, E, N, D, M, O, R, Y, C1, C2, C3, C4, =_out_ga(C4, M)) → =\=_IN_GG(M, 0)
U53_AAAAAAAA(S, E, N, D, M, O, R, Y, C1, C2, C3, C4, =\=_out_gg(M, 0)) → U54_AAAAAAAA(S, E, N, D, M, O, R, Y, C1, C2, C3, C4, domain_in_gg(.(S, .(E, .(N, .(D, .(M, .(O, .(R, .(Y, [])))))))), .(0, .(1, .(2, .(3, .(4, .(5, .(6, .(7, .(8, .(9, []))))))))))))
U53_AAAAAAAA(S, E, N, D, M, O, R, Y, C1, C2, C3, C4, =\=_out_gg(M, 0)) → DOMAIN_IN_GG(.(S, .(E, .(N, .(D, .(M, .(O, .(R, .(Y, [])))))))), .(0, .(1, .(2, .(3, .(4, .(5, .(6, .(7, .(8, .(9, [])))))))))))
DOMAIN_IN_GG(.(X1, R), L) → U65_GG(X1, R, L, del_in_aga(X1, L, NL))
DOMAIN_IN_GG(.(X1, R), L) → DEL_IN_AGA(X1, L, NL)
DEL_IN_AGA(X, .(Y, T), .(Y, NT)) → U67_AGA(X, Y, T, NT, del_in_aga(X, T, NT))
DEL_IN_AGA(X, .(Y, T), .(Y, NT)) → DEL_IN_AGA(X, T, NT)
U65_GG(X1, R, L, del_out_aga(X1, L, NL)) → U66_GG(X1, R, L, domain_in_gg(R, NL))
U65_GG(X1, R, L, del_out_aga(X1, L, NL)) → DOMAIN_IN_GG(R, NL)
U54_AAAAAAAA(S, E, N, D, M, O, R, Y, C1, C2, C3, C4, domain_out_gg(.(S, .(E, .(N, .(D, .(M, .(O, .(R, .(Y, [])))))))), .(0, .(1, .(2, .(3, .(4, .(5, .(6, .(7, .(8, .(9, [])))))))))))) → U55_AAAAAAAA(S, E, N, D, M, O, R, Y, C1, C2, C3, C4, =\=_in_ag(S, 0))
U54_AAAAAAAA(S, E, N, D, M, O, R, Y, C1, C2, C3, C4, domain_out_gg(.(S, .(E, .(N, .(D, .(M, .(O, .(R, .(Y, [])))))))), .(0, .(1, .(2, .(3, .(4, .(5, .(6, .(7, .(8, .(9, [])))))))))))) → =\=_IN_AG(S, 0)
U55_AAAAAAAA(S, E, N, D, M, O, R, Y, C1, C2, C3, C4, =\=_out_ag(S, 0)) → U56_AAAAAAAA(S, E, N, D, M, O, R, Y, C1, C2, C3, calc_in_gagga(C3, S, M, C4, O))
U55_AAAAAAAA(S, E, N, D, M, O, R, Y, C1, C2, C3, C4, =\=_out_ag(S, 0)) → CALC_IN_GAGGA(C3, S, M, C4, O)
CALC_IN_GAGGA(C0, D, E, C1, Y) → U60_GAGGA(C0, D, E, C1, Y, sum_in_gaa(C0, D, CD))
CALC_IN_GAGGA(C0, D, E, C1, Y) → SUM_IN_GAA(C0, D, CD)
SUM_IN_GAA(X, Y, Z) → U64_GAA(X, Y, Z, is_in_ag(Z, +(X, Y)))
SUM_IN_GAA(X, Y, Z) → IS_IN_AG(Z, +(X, Y))
U60_GAGGA(C0, D, E, C1, Y, sum_out_gaa(C0, D, CD)) → U61_GAGGA(C0, D, E, C1, Y, sum_in_aga(CD, E, S))
U60_GAGGA(C0, D, E, C1, Y, sum_out_gaa(C0, D, CD)) → SUM_IN_AGA(CD, E, S)
SUM_IN_AGA(X, Y, Z) → U64_AGA(X, Y, Z, is_in_ag(Z, +(X, Y)))
SUM_IN_AGA(X, Y, Z) → IS_IN_AG(Z, +(X, Y))
U61_GAGGA(C0, D, E, C1, Y, sum_out_aga(CD, E, S)) → U62_GAGGA(C0, D, E, C1, Y, S, carry10_in_ga(C1, C10))
U61_GAGGA(C0, D, E, C1, Y, sum_out_aga(CD, E, S)) → CARRY10_IN_GA(C1, C10)
U62_GAGGA(C0, D, E, C1, Y, S, carry10_out_ga(C1, C10)) → U63_GAGGA(C0, D, E, C1, Y, sum_in_gaa(C10, Y, S))
U62_GAGGA(C0, D, E, C1, Y, S, carry10_out_ga(C1, C10)) → SUM_IN_GAA(C10, Y, S)
U56_AAAAAAAA(S, E, N, D, M, O, R, Y, C1, C2, C3, calc_out_gagga(C3, S, M, C4, O)) → U57_AAAAAAAA(S, E, N, D, M, O, R, Y, C1, C2, calc_in_gaaga(C2, E, O, C3, N))
U56_AAAAAAAA(S, E, N, D, M, O, R, Y, C1, C2, C3, calc_out_gagga(C3, S, M, C4, O)) → CALC_IN_GAAGA(C2, E, O, C3, N)
CALC_IN_GAAGA(C0, D, E, C1, Y) → U60_GAAGA(C0, D, E, C1, Y, sum_in_gaa(C0, D, CD))
CALC_IN_GAAGA(C0, D, E, C1, Y) → SUM_IN_GAA(C0, D, CD)
U60_GAAGA(C0, D, E, C1, Y, sum_out_gaa(C0, D, CD)) → U61_GAAGA(C0, D, E, C1, Y, sum_in_aaa(CD, E, S))
U60_GAAGA(C0, D, E, C1, Y, sum_out_gaa(C0, D, CD)) → SUM_IN_AAA(CD, E, S)
SUM_IN_AAA(X, Y, Z) → U64_AAA(X, Y, Z, is_in_ag(Z, +(X, Y)))
SUM_IN_AAA(X, Y, Z) → IS_IN_AG(Z, +(X, Y))
U61_GAAGA(C0, D, E, C1, Y, sum_out_aaa(CD, E, S)) → U62_GAAGA(C0, D, E, C1, Y, S, carry10_in_ga(C1, C10))
U61_GAAGA(C0, D, E, C1, Y, sum_out_aaa(CD, E, S)) → CARRY10_IN_GA(C1, C10)
U62_GAAGA(C0, D, E, C1, Y, S, carry10_out_ga(C1, C10)) → U63_GAAGA(C0, D, E, C1, Y, sum_in_gaa(C10, Y, S))
U62_GAAGA(C0, D, E, C1, Y, S, carry10_out_ga(C1, C10)) → SUM_IN_GAA(C10, Y, S)
U57_AAAAAAAA(S, E, N, D, M, O, R, Y, C1, C2, calc_out_gaaga(C2, E, O, C3, N)) → U58_AAAAAAAA(S, E, N, D, M, O, R, Y, C1, calc_in_gaaga(C1, N, R, C2, E))
U57_AAAAAAAA(S, E, N, D, M, O, R, Y, C1, C2, calc_out_gaaga(C2, E, O, C3, N)) → CALC_IN_GAAGA(C1, N, R, C2, E)
U58_AAAAAAAA(S, E, N, D, M, O, R, Y, C1, calc_out_gaaga(C1, N, R, C2, E)) → U59_AAAAAAAA(S, E, N, D, M, O, R, Y, calc_in_gaaga(0, D, E, C1, Y))
U58_AAAAAAAA(S, E, N, D, M, O, R, Y, C1, calc_out_gaaga(C1, N, R, C2, E)) → CALC_IN_GAAGA(0, D, E, C1, Y)

The TRS R consists of the following rules:

money_in_aaaaaaaa(S, E, N, D, M, O, R, Y) → U48_aaaaaaaa(S, E, N, D, M, O, R, Y, carry_in_a(C1))
carry_in_a(1) → carry_out_a(1)
carry_in_a(0) → carry_out_a(0)
U48_aaaaaaaa(S, E, N, D, M, O, R, Y, carry_out_a(C1)) → U49_aaaaaaaa(S, E, N, D, M, O, R, Y, C1, carry_in_a(C2))
U49_aaaaaaaa(S, E, N, D, M, O, R, Y, C1, carry_out_a(C2)) → U50_aaaaaaaa(S, E, N, D, M, O, R, Y, C1, C2, carry_in_a(C3))
U50_aaaaaaaa(S, E, N, D, M, O, R, Y, C1, C2, carry_out_a(C3)) → U51_aaaaaaaa(S, E, N, D, M, O, R, Y, C1, C2, C3, carry_in_a(C4))
U51_aaaaaaaa(S, E, N, D, M, O, R, Y, C1, C2, C3, carry_out_a(C4)) → U52_aaaaaaaa(S, E, N, D, M, O, R, Y, C1, C2, C3, C4, =_in_ga(C4, M))
=_in_ga(X, X) → =_out_ga(X, X)
U52_aaaaaaaa(S, E, N, D, M, O, R, Y, C1, C2, C3, C4, =_out_ga(C4, M)) → U53_aaaaaaaa(S, E, N, D, M, O, R, Y, C1, C2, C3, C4, =\=_in_gg(M, 0))
=\=_in_gg(X0, X1) → =\=_out_gg(X0, X1)
U53_aaaaaaaa(S, E, N, D, M, O, R, Y, C1, C2, C3, C4, =\=_out_gg(M, 0)) → U54_aaaaaaaa(S, E, N, D, M, O, R, Y, C1, C2, C3, C4, domain_in_gg(.(S, .(E, .(N, .(D, .(M, .(O, .(R, .(Y, [])))))))), .(0, .(1, .(2, .(3, .(4, .(5, .(6, .(7, .(8, .(9, []))))))))))))
domain_in_gg([], X3) → domain_out_gg([], X3)
domain_in_gg(.(X1, R), L) → U65_gg(X1, R, L, del_in_aga(X1, L, NL))
del_in_aga(X, .(X, T), T) → del_out_aga(X, .(X, T), T)
del_in_aga(X, .(Y, T), .(Y, NT)) → U67_aga(X, Y, T, NT, del_in_aga(X, T, NT))
U67_aga(X, Y, T, NT, del_out_aga(X, T, NT)) → del_out_aga(X, .(Y, T), .(Y, NT))
U65_gg(X1, R, L, del_out_aga(X1, L, NL)) → U66_gg(X1, R, L, domain_in_gg(R, NL))
U66_gg(X1, R, L, domain_out_gg(R, NL)) → domain_out_gg(.(X1, R), L)
U54_aaaaaaaa(S, E, N, D, M, O, R, Y, C1, C2, C3, C4, domain_out_gg(.(S, .(E, .(N, .(D, .(M, .(O, .(R, .(Y, [])))))))), .(0, .(1, .(2, .(3, .(4, .(5, .(6, .(7, .(8, .(9, [])))))))))))) → U55_aaaaaaaa(S, E, N, D, M, O, R, Y, C1, C2, C3, C4, =\=_in_ag(S, 0))
=\=_in_ag(X0, X1) → =\=_out_ag(X0, X1)
U55_aaaaaaaa(S, E, N, D, M, O, R, Y, C1, C2, C3, C4, =\=_out_ag(S, 0)) → U56_aaaaaaaa(S, E, N, D, M, O, R, Y, C1, C2, C3, calc_in_gagga(C3, S, M, C4, O))
calc_in_gagga(C0, D, E, C1, Y) → U60_gagga(C0, D, E, C1, Y, sum_in_gaa(C0, D, CD))
sum_in_gaa(X, Y, Z) → U64_gaa(X, Y, Z, is_in_ag(Z, +(X, Y)))
is_in_ag(X0, X1) → is_out_ag(X0, X1)
U64_gaa(X, Y, Z, is_out_ag(Z, +(X, Y))) → sum_out_gaa(X, Y, Z)
U60_gagga(C0, D, E, C1, Y, sum_out_gaa(C0, D, CD)) → U61_gagga(C0, D, E, C1, Y, sum_in_aga(CD, E, S))
sum_in_aga(X, Y, Z) → U64_aga(X, Y, Z, is_in_ag(Z, +(X, Y)))
U64_aga(X, Y, Z, is_out_ag(Z, +(X, Y))) → sum_out_aga(X, Y, Z)
U61_gagga(C0, D, E, C1, Y, sum_out_aga(CD, E, S)) → U62_gagga(C0, D, E, C1, Y, S, carry10_in_ga(C1, C10))
carry10_in_ga(0, 0) → carry10_out_ga(0, 0)
carry10_in_ga(1, 10) → carry10_out_ga(1, 10)
U62_gagga(C0, D, E, C1, Y, S, carry10_out_ga(C1, C10)) → U63_gagga(C0, D, E, C1, Y, sum_in_gaa(C10, Y, S))
U63_gagga(C0, D, E, C1, Y, sum_out_gaa(C10, Y, S)) → calc_out_gagga(C0, D, E, C1, Y)
U56_aaaaaaaa(S, E, N, D, M, O, R, Y, C1, C2, C3, calc_out_gagga(C3, S, M, C4, O)) → U57_aaaaaaaa(S, E, N, D, M, O, R, Y, C1, C2, calc_in_gaaga(C2, E, O, C3, N))
calc_in_gaaga(C0, D, E, C1, Y) → U60_gaaga(C0, D, E, C1, Y, sum_in_gaa(C0, D, CD))
U60_gaaga(C0, D, E, C1, Y, sum_out_gaa(C0, D, CD)) → U61_gaaga(C0, D, E, C1, Y, sum_in_aaa(CD, E, S))
sum_in_aaa(X, Y, Z) → U64_aaa(X, Y, Z, is_in_ag(Z, +(X, Y)))
U64_aaa(X, Y, Z, is_out_ag(Z, +(X, Y))) → sum_out_aaa(X, Y, Z)
U61_gaaga(C0, D, E, C1, Y, sum_out_aaa(CD, E, S)) → U62_gaaga(C0, D, E, C1, Y, S, carry10_in_ga(C1, C10))
U62_gaaga(C0, D, E, C1, Y, S, carry10_out_ga(C1, C10)) → U63_gaaga(C0, D, E, C1, Y, sum_in_gaa(C10, Y, S))
U63_gaaga(C0, D, E, C1, Y, sum_out_gaa(C10, Y, S)) → calc_out_gaaga(C0, D, E, C1, Y)
U57_aaaaaaaa(S, E, N, D, M, O, R, Y, C1, C2, calc_out_gaaga(C2, E, O, C3, N)) → U58_aaaaaaaa(S, E, N, D, M, O, R, Y, C1, calc_in_gaaga(C1, N, R, C2, E))
U58_aaaaaaaa(S, E, N, D, M, O, R, Y, C1, calc_out_gaaga(C1, N, R, C2, E)) → U59_aaaaaaaa(S, E, N, D, M, O, R, Y, calc_in_gaaga(0, D, E, C1, Y))
U59_aaaaaaaa(S, E, N, D, M, O, R, Y, calc_out_gaaga(0, D, E, C1, Y)) → money_out_aaaaaaaa(S, E, N, D, M, O, R, Y)

The argument filtering Pi contains the following mapping:
money_in_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8)  =  money_in_aaaaaaaa
U48_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U48_aaaaaaaa(x9)
carry_in_a(x1)  =  carry_in_a
carry_out_a(x1)  =  carry_out_a(x1)
U49_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)  =  U49_aaaaaaaa(x9, x10)
U50_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11)  =  U50_aaaaaaaa(x9, x10, x11)
U51_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12)  =  U51_aaaaaaaa(x9, x10, x11, x12)
U52_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13)  =  U52_aaaaaaaa(x9, x10, x11, x12, x13)
=_in_ga(x1, x2)  =  =_in_ga(x1)
=_out_ga(x1, x2)  =  =_out_ga(x2)
U53_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13)  =  U53_aaaaaaaa(x5, x9, x10, x11, x12, x13)
=\=_in_gg(x1, x2)  =  =\=_in_gg(x1, x2)
=\=_out_gg(x1, x2)  =  =\=_out_gg
0  =  0
U54_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13)  =  U54_aaaaaaaa(x5, x9, x10, x11, x12, x13)
domain_in_gg(x1, x2)  =  domain_in_gg(x1, x2)
.(x1, x2)  =  .(x2)
[]  =  []
domain_out_gg(x1, x2)  =  domain_out_gg
U65_gg(x1, x2, x3, x4)  =  U65_gg(x2, x4)
del_in_aga(x1, x2, x3)  =  del_in_aga(x2)
del_out_aga(x1, x2, x3)  =  del_out_aga(x3)
U67_aga(x1, x2, x3, x4, x5)  =  U67_aga(x5)
U66_gg(x1, x2, x3, x4)  =  U66_gg(x4)
U55_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13)  =  U55_aaaaaaaa(x5, x9, x10, x11, x12, x13)
=\=_in_ag(x1, x2)  =  =\=_in_ag(x2)
=\=_out_ag(x1, x2)  =  =\=_out_ag
U56_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12)  =  U56_aaaaaaaa(x5, x9, x10, x11, x12)
calc_in_gagga(x1, x2, x3, x4, x5)  =  calc_in_gagga(x1, x3, x4)
U60_gagga(x1, x2, x3, x4, x5, x6)  =  U60_gagga(x3, x4, x6)
sum_in_gaa(x1, x2, x3)  =  sum_in_gaa(x1)
U64_gaa(x1, x2, x3, x4)  =  U64_gaa(x4)
is_in_ag(x1, x2)  =  is_in_ag(x2)
+(x1, x2)  =  +
is_out_ag(x1, x2)  =  is_out_ag
sum_out_gaa(x1, x2, x3)  =  sum_out_gaa
U61_gagga(x1, x2, x3, x4, x5, x6)  =  U61_gagga(x4, x6)
sum_in_aga(x1, x2, x3)  =  sum_in_aga(x2)
U64_aga(x1, x2, x3, x4)  =  U64_aga(x4)
sum_out_aga(x1, x2, x3)  =  sum_out_aga
U62_gagga(x1, x2, x3, x4, x5, x6, x7)  =  U62_gagga(x7)
carry10_in_ga(x1, x2)  =  carry10_in_ga(x1)
carry10_out_ga(x1, x2)  =  carry10_out_ga(x2)
1  =  1
U63_gagga(x1, x2, x3, x4, x5, x6)  =  U63_gagga(x6)
calc_out_gagga(x1, x2, x3, x4, x5)  =  calc_out_gagga
U57_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11)  =  U57_aaaaaaaa(x5, x9, x10, x11)
calc_in_gaaga(x1, x2, x3, x4, x5)  =  calc_in_gaaga(x1, x4)
U60_gaaga(x1, x2, x3, x4, x5, x6)  =  U60_gaaga(x4, x6)
U61_gaaga(x1, x2, x3, x4, x5, x6)  =  U61_gaaga(x4, x6)
sum_in_aaa(x1, x2, x3)  =  sum_in_aaa
U64_aaa(x1, x2, x3, x4)  =  U64_aaa(x4)
sum_out_aaa(x1, x2, x3)  =  sum_out_aaa
U62_gaaga(x1, x2, x3, x4, x5, x6, x7)  =  U62_gaaga(x7)
U63_gaaga(x1, x2, x3, x4, x5, x6)  =  U63_gaaga(x6)
calc_out_gaaga(x1, x2, x3, x4, x5)  =  calc_out_gaaga
U58_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)  =  U58_aaaaaaaa(x5, x9, x10)
U59_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U59_aaaaaaaa(x5, x9)
money_out_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8)  =  money_out_aaaaaaaa(x5)
MONEY_IN_AAAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8)  =  MONEY_IN_AAAAAAAA
U48_AAAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U48_AAAAAAAA(x9)
CARRY_IN_A(x1)  =  CARRY_IN_A
U49_AAAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)  =  U49_AAAAAAAA(x9, x10)
U50_AAAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11)  =  U50_AAAAAAAA(x9, x10, x11)
U51_AAAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12)  =  U51_AAAAAAAA(x9, x10, x11, x12)
U52_AAAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13)  =  U52_AAAAAAAA(x9, x10, x11, x12, x13)
=_IN_GA(x1, x2)  =  =_IN_GA(x1)
U53_AAAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13)  =  U53_AAAAAAAA(x5, x9, x10, x11, x12, x13)
=\=_IN_GG(x1, x2)  =  =\=_IN_GG(x1, x2)
U54_AAAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13)  =  U54_AAAAAAAA(x5, x9, x10, x11, x12, x13)
DOMAIN_IN_GG(x1, x2)  =  DOMAIN_IN_GG(x1, x2)
U65_GG(x1, x2, x3, x4)  =  U65_GG(x2, x4)
DEL_IN_AGA(x1, x2, x3)  =  DEL_IN_AGA(x2)
U67_AGA(x1, x2, x3, x4, x5)  =  U67_AGA(x5)
U66_GG(x1, x2, x3, x4)  =  U66_GG(x4)
U55_AAAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13)  =  U55_AAAAAAAA(x5, x9, x10, x11, x12, x13)
=\=_IN_AG(x1, x2)  =  =\=_IN_AG(x2)
U56_AAAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12)  =  U56_AAAAAAAA(x5, x9, x10, x11, x12)
CALC_IN_GAGGA(x1, x2, x3, x4, x5)  =  CALC_IN_GAGGA(x1, x3, x4)
U60_GAGGA(x1, x2, x3, x4, x5, x6)  =  U60_GAGGA(x3, x4, x6)
SUM_IN_GAA(x1, x2, x3)  =  SUM_IN_GAA(x1)
U64_GAA(x1, x2, x3, x4)  =  U64_GAA(x4)
IS_IN_AG(x1, x2)  =  IS_IN_AG(x2)
U61_GAGGA(x1, x2, x3, x4, x5, x6)  =  U61_GAGGA(x4, x6)
SUM_IN_AGA(x1, x2, x3)  =  SUM_IN_AGA(x2)
U64_AGA(x1, x2, x3, x4)  =  U64_AGA(x4)
U62_GAGGA(x1, x2, x3, x4, x5, x6, x7)  =  U62_GAGGA(x7)
CARRY10_IN_GA(x1, x2)  =  CARRY10_IN_GA(x1)
U63_GAGGA(x1, x2, x3, x4, x5, x6)  =  U63_GAGGA(x6)
U57_AAAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11)  =  U57_AAAAAAAA(x5, x9, x10, x11)
CALC_IN_GAAGA(x1, x2, x3, x4, x5)  =  CALC_IN_GAAGA(x1, x4)
U60_GAAGA(x1, x2, x3, x4, x5, x6)  =  U60_GAAGA(x4, x6)
U61_GAAGA(x1, x2, x3, x4, x5, x6)  =  U61_GAAGA(x4, x6)
SUM_IN_AAA(x1, x2, x3)  =  SUM_IN_AAA
U64_AAA(x1, x2, x3, x4)  =  U64_AAA(x4)
U62_GAAGA(x1, x2, x3, x4, x5, x6, x7)  =  U62_GAAGA(x7)
U63_GAAGA(x1, x2, x3, x4, x5, x6)  =  U63_GAAGA(x6)
U58_AAAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)  =  U58_AAAAAAAA(x5, x9, x10)
U59_AAAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U59_AAAAAAAA(x5, x9)

We have to consider all (P,R,Pi)-chains

(8) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

MONEY_IN_AAAAAAAA(S, E, N, D, M, O, R, Y) → U48_AAAAAAAA(S, E, N, D, M, O, R, Y, carry_in_a(C1))
MONEY_IN_AAAAAAAA(S, E, N, D, M, O, R, Y) → CARRY_IN_A(C1)
U48_AAAAAAAA(S, E, N, D, M, O, R, Y, carry_out_a(C1)) → U49_AAAAAAAA(S, E, N, D, M, O, R, Y, C1, carry_in_a(C2))
U48_AAAAAAAA(S, E, N, D, M, O, R, Y, carry_out_a(C1)) → CARRY_IN_A(C2)
U49_AAAAAAAA(S, E, N, D, M, O, R, Y, C1, carry_out_a(C2)) → U50_AAAAAAAA(S, E, N, D, M, O, R, Y, C1, C2, carry_in_a(C3))
U49_AAAAAAAA(S, E, N, D, M, O, R, Y, C1, carry_out_a(C2)) → CARRY_IN_A(C3)
U50_AAAAAAAA(S, E, N, D, M, O, R, Y, C1, C2, carry_out_a(C3)) → U51_AAAAAAAA(S, E, N, D, M, O, R, Y, C1, C2, C3, carry_in_a(C4))
U50_AAAAAAAA(S, E, N, D, M, O, R, Y, C1, C2, carry_out_a(C3)) → CARRY_IN_A(C4)
U51_AAAAAAAA(S, E, N, D, M, O, R, Y, C1, C2, C3, carry_out_a(C4)) → U52_AAAAAAAA(S, E, N, D, M, O, R, Y, C1, C2, C3, C4, =_in_ga(C4, M))
U51_AAAAAAAA(S, E, N, D, M, O, R, Y, C1, C2, C3, carry_out_a(C4)) → =_IN_GA(C4, M)
U52_AAAAAAAA(S, E, N, D, M, O, R, Y, C1, C2, C3, C4, =_out_ga(C4, M)) → U53_AAAAAAAA(S, E, N, D, M, O, R, Y, C1, C2, C3, C4, =\=_in_gg(M, 0))
U52_AAAAAAAA(S, E, N, D, M, O, R, Y, C1, C2, C3, C4, =_out_ga(C4, M)) → =\=_IN_GG(M, 0)
U53_AAAAAAAA(S, E, N, D, M, O, R, Y, C1, C2, C3, C4, =\=_out_gg(M, 0)) → U54_AAAAAAAA(S, E, N, D, M, O, R, Y, C1, C2, C3, C4, domain_in_gg(.(S, .(E, .(N, .(D, .(M, .(O, .(R, .(Y, [])))))))), .(0, .(1, .(2, .(3, .(4, .(5, .(6, .(7, .(8, .(9, []))))))))))))
U53_AAAAAAAA(S, E, N, D, M, O, R, Y, C1, C2, C3, C4, =\=_out_gg(M, 0)) → DOMAIN_IN_GG(.(S, .(E, .(N, .(D, .(M, .(O, .(R, .(Y, [])))))))), .(0, .(1, .(2, .(3, .(4, .(5, .(6, .(7, .(8, .(9, [])))))))))))
DOMAIN_IN_GG(.(X1, R), L) → U65_GG(X1, R, L, del_in_aga(X1, L, NL))
DOMAIN_IN_GG(.(X1, R), L) → DEL_IN_AGA(X1, L, NL)
DEL_IN_AGA(X, .(Y, T), .(Y, NT)) → U67_AGA(X, Y, T, NT, del_in_aga(X, T, NT))
DEL_IN_AGA(X, .(Y, T), .(Y, NT)) → DEL_IN_AGA(X, T, NT)
U65_GG(X1, R, L, del_out_aga(X1, L, NL)) → U66_GG(X1, R, L, domain_in_gg(R, NL))
U65_GG(X1, R, L, del_out_aga(X1, L, NL)) → DOMAIN_IN_GG(R, NL)
U54_AAAAAAAA(S, E, N, D, M, O, R, Y, C1, C2, C3, C4, domain_out_gg(.(S, .(E, .(N, .(D, .(M, .(O, .(R, .(Y, [])))))))), .(0, .(1, .(2, .(3, .(4, .(5, .(6, .(7, .(8, .(9, [])))))))))))) → U55_AAAAAAAA(S, E, N, D, M, O, R, Y, C1, C2, C3, C4, =\=_in_ag(S, 0))
U54_AAAAAAAA(S, E, N, D, M, O, R, Y, C1, C2, C3, C4, domain_out_gg(.(S, .(E, .(N, .(D, .(M, .(O, .(R, .(Y, [])))))))), .(0, .(1, .(2, .(3, .(4, .(5, .(6, .(7, .(8, .(9, [])))))))))))) → =\=_IN_AG(S, 0)
U55_AAAAAAAA(S, E, N, D, M, O, R, Y, C1, C2, C3, C4, =\=_out_ag(S, 0)) → U56_AAAAAAAA(S, E, N, D, M, O, R, Y, C1, C2, C3, calc_in_gagga(C3, S, M, C4, O))
U55_AAAAAAAA(S, E, N, D, M, O, R, Y, C1, C2, C3, C4, =\=_out_ag(S, 0)) → CALC_IN_GAGGA(C3, S, M, C4, O)
CALC_IN_GAGGA(C0, D, E, C1, Y) → U60_GAGGA(C0, D, E, C1, Y, sum_in_gaa(C0, D, CD))
CALC_IN_GAGGA(C0, D, E, C1, Y) → SUM_IN_GAA(C0, D, CD)
SUM_IN_GAA(X, Y, Z) → U64_GAA(X, Y, Z, is_in_ag(Z, +(X, Y)))
SUM_IN_GAA(X, Y, Z) → IS_IN_AG(Z, +(X, Y))
U60_GAGGA(C0, D, E, C1, Y, sum_out_gaa(C0, D, CD)) → U61_GAGGA(C0, D, E, C1, Y, sum_in_aga(CD, E, S))
U60_GAGGA(C0, D, E, C1, Y, sum_out_gaa(C0, D, CD)) → SUM_IN_AGA(CD, E, S)
SUM_IN_AGA(X, Y, Z) → U64_AGA(X, Y, Z, is_in_ag(Z, +(X, Y)))
SUM_IN_AGA(X, Y, Z) → IS_IN_AG(Z, +(X, Y))
U61_GAGGA(C0, D, E, C1, Y, sum_out_aga(CD, E, S)) → U62_GAGGA(C0, D, E, C1, Y, S, carry10_in_ga(C1, C10))
U61_GAGGA(C0, D, E, C1, Y, sum_out_aga(CD, E, S)) → CARRY10_IN_GA(C1, C10)
U62_GAGGA(C0, D, E, C1, Y, S, carry10_out_ga(C1, C10)) → U63_GAGGA(C0, D, E, C1, Y, sum_in_gaa(C10, Y, S))
U62_GAGGA(C0, D, E, C1, Y, S, carry10_out_ga(C1, C10)) → SUM_IN_GAA(C10, Y, S)
U56_AAAAAAAA(S, E, N, D, M, O, R, Y, C1, C2, C3, calc_out_gagga(C3, S, M, C4, O)) → U57_AAAAAAAA(S, E, N, D, M, O, R, Y, C1, C2, calc_in_gaaga(C2, E, O, C3, N))
U56_AAAAAAAA(S, E, N, D, M, O, R, Y, C1, C2, C3, calc_out_gagga(C3, S, M, C4, O)) → CALC_IN_GAAGA(C2, E, O, C3, N)
CALC_IN_GAAGA(C0, D, E, C1, Y) → U60_GAAGA(C0, D, E, C1, Y, sum_in_gaa(C0, D, CD))
CALC_IN_GAAGA(C0, D, E, C1, Y) → SUM_IN_GAA(C0, D, CD)
U60_GAAGA(C0, D, E, C1, Y, sum_out_gaa(C0, D, CD)) → U61_GAAGA(C0, D, E, C1, Y, sum_in_aaa(CD, E, S))
U60_GAAGA(C0, D, E, C1, Y, sum_out_gaa(C0, D, CD)) → SUM_IN_AAA(CD, E, S)
SUM_IN_AAA(X, Y, Z) → U64_AAA(X, Y, Z, is_in_ag(Z, +(X, Y)))
SUM_IN_AAA(X, Y, Z) → IS_IN_AG(Z, +(X, Y))
U61_GAAGA(C0, D, E, C1, Y, sum_out_aaa(CD, E, S)) → U62_GAAGA(C0, D, E, C1, Y, S, carry10_in_ga(C1, C10))
U61_GAAGA(C0, D, E, C1, Y, sum_out_aaa(CD, E, S)) → CARRY10_IN_GA(C1, C10)
U62_GAAGA(C0, D, E, C1, Y, S, carry10_out_ga(C1, C10)) → U63_GAAGA(C0, D, E, C1, Y, sum_in_gaa(C10, Y, S))
U62_GAAGA(C0, D, E, C1, Y, S, carry10_out_ga(C1, C10)) → SUM_IN_GAA(C10, Y, S)
U57_AAAAAAAA(S, E, N, D, M, O, R, Y, C1, C2, calc_out_gaaga(C2, E, O, C3, N)) → U58_AAAAAAAA(S, E, N, D, M, O, R, Y, C1, calc_in_gaaga(C1, N, R, C2, E))
U57_AAAAAAAA(S, E, N, D, M, O, R, Y, C1, C2, calc_out_gaaga(C2, E, O, C3, N)) → CALC_IN_GAAGA(C1, N, R, C2, E)
U58_AAAAAAAA(S, E, N, D, M, O, R, Y, C1, calc_out_gaaga(C1, N, R, C2, E)) → U59_AAAAAAAA(S, E, N, D, M, O, R, Y, calc_in_gaaga(0, D, E, C1, Y))
U58_AAAAAAAA(S, E, N, D, M, O, R, Y, C1, calc_out_gaaga(C1, N, R, C2, E)) → CALC_IN_GAAGA(0, D, E, C1, Y)

The TRS R consists of the following rules:

money_in_aaaaaaaa(S, E, N, D, M, O, R, Y) → U48_aaaaaaaa(S, E, N, D, M, O, R, Y, carry_in_a(C1))
carry_in_a(1) → carry_out_a(1)
carry_in_a(0) → carry_out_a(0)
U48_aaaaaaaa(S, E, N, D, M, O, R, Y, carry_out_a(C1)) → U49_aaaaaaaa(S, E, N, D, M, O, R, Y, C1, carry_in_a(C2))
U49_aaaaaaaa(S, E, N, D, M, O, R, Y, C1, carry_out_a(C2)) → U50_aaaaaaaa(S, E, N, D, M, O, R, Y, C1, C2, carry_in_a(C3))
U50_aaaaaaaa(S, E, N, D, M, O, R, Y, C1, C2, carry_out_a(C3)) → U51_aaaaaaaa(S, E, N, D, M, O, R, Y, C1, C2, C3, carry_in_a(C4))
U51_aaaaaaaa(S, E, N, D, M, O, R, Y, C1, C2, C3, carry_out_a(C4)) → U52_aaaaaaaa(S, E, N, D, M, O, R, Y, C1, C2, C3, C4, =_in_ga(C4, M))
=_in_ga(X, X) → =_out_ga(X, X)
U52_aaaaaaaa(S, E, N, D, M, O, R, Y, C1, C2, C3, C4, =_out_ga(C4, M)) → U53_aaaaaaaa(S, E, N, D, M, O, R, Y, C1, C2, C3, C4, =\=_in_gg(M, 0))
=\=_in_gg(X0, X1) → =\=_out_gg(X0, X1)
U53_aaaaaaaa(S, E, N, D, M, O, R, Y, C1, C2, C3, C4, =\=_out_gg(M, 0)) → U54_aaaaaaaa(S, E, N, D, M, O, R, Y, C1, C2, C3, C4, domain_in_gg(.(S, .(E, .(N, .(D, .(M, .(O, .(R, .(Y, [])))))))), .(0, .(1, .(2, .(3, .(4, .(5, .(6, .(7, .(8, .(9, []))))))))))))
domain_in_gg([], X3) → domain_out_gg([], X3)
domain_in_gg(.(X1, R), L) → U65_gg(X1, R, L, del_in_aga(X1, L, NL))
del_in_aga(X, .(X, T), T) → del_out_aga(X, .(X, T), T)
del_in_aga(X, .(Y, T), .(Y, NT)) → U67_aga(X, Y, T, NT, del_in_aga(X, T, NT))
U67_aga(X, Y, T, NT, del_out_aga(X, T, NT)) → del_out_aga(X, .(Y, T), .(Y, NT))
U65_gg(X1, R, L, del_out_aga(X1, L, NL)) → U66_gg(X1, R, L, domain_in_gg(R, NL))
U66_gg(X1, R, L, domain_out_gg(R, NL)) → domain_out_gg(.(X1, R), L)
U54_aaaaaaaa(S, E, N, D, M, O, R, Y, C1, C2, C3, C4, domain_out_gg(.(S, .(E, .(N, .(D, .(M, .(O, .(R, .(Y, [])))))))), .(0, .(1, .(2, .(3, .(4, .(5, .(6, .(7, .(8, .(9, [])))))))))))) → U55_aaaaaaaa(S, E, N, D, M, O, R, Y, C1, C2, C3, C4, =\=_in_ag(S, 0))
=\=_in_ag(X0, X1) → =\=_out_ag(X0, X1)
U55_aaaaaaaa(S, E, N, D, M, O, R, Y, C1, C2, C3, C4, =\=_out_ag(S, 0)) → U56_aaaaaaaa(S, E, N, D, M, O, R, Y, C1, C2, C3, calc_in_gagga(C3, S, M, C4, O))
calc_in_gagga(C0, D, E, C1, Y) → U60_gagga(C0, D, E, C1, Y, sum_in_gaa(C0, D, CD))
sum_in_gaa(X, Y, Z) → U64_gaa(X, Y, Z, is_in_ag(Z, +(X, Y)))
is_in_ag(X0, X1) → is_out_ag(X0, X1)
U64_gaa(X, Y, Z, is_out_ag(Z, +(X, Y))) → sum_out_gaa(X, Y, Z)
U60_gagga(C0, D, E, C1, Y, sum_out_gaa(C0, D, CD)) → U61_gagga(C0, D, E, C1, Y, sum_in_aga(CD, E, S))
sum_in_aga(X, Y, Z) → U64_aga(X, Y, Z, is_in_ag(Z, +(X, Y)))
U64_aga(X, Y, Z, is_out_ag(Z, +(X, Y))) → sum_out_aga(X, Y, Z)
U61_gagga(C0, D, E, C1, Y, sum_out_aga(CD, E, S)) → U62_gagga(C0, D, E, C1, Y, S, carry10_in_ga(C1, C10))
carry10_in_ga(0, 0) → carry10_out_ga(0, 0)
carry10_in_ga(1, 10) → carry10_out_ga(1, 10)
U62_gagga(C0, D, E, C1, Y, S, carry10_out_ga(C1, C10)) → U63_gagga(C0, D, E, C1, Y, sum_in_gaa(C10, Y, S))
U63_gagga(C0, D, E, C1, Y, sum_out_gaa(C10, Y, S)) → calc_out_gagga(C0, D, E, C1, Y)
U56_aaaaaaaa(S, E, N, D, M, O, R, Y, C1, C2, C3, calc_out_gagga(C3, S, M, C4, O)) → U57_aaaaaaaa(S, E, N, D, M, O, R, Y, C1, C2, calc_in_gaaga(C2, E, O, C3, N))
calc_in_gaaga(C0, D, E, C1, Y) → U60_gaaga(C0, D, E, C1, Y, sum_in_gaa(C0, D, CD))
U60_gaaga(C0, D, E, C1, Y, sum_out_gaa(C0, D, CD)) → U61_gaaga(C0, D, E, C1, Y, sum_in_aaa(CD, E, S))
sum_in_aaa(X, Y, Z) → U64_aaa(X, Y, Z, is_in_ag(Z, +(X, Y)))
U64_aaa(X, Y, Z, is_out_ag(Z, +(X, Y))) → sum_out_aaa(X, Y, Z)
U61_gaaga(C0, D, E, C1, Y, sum_out_aaa(CD, E, S)) → U62_gaaga(C0, D, E, C1, Y, S, carry10_in_ga(C1, C10))
U62_gaaga(C0, D, E, C1, Y, S, carry10_out_ga(C1, C10)) → U63_gaaga(C0, D, E, C1, Y, sum_in_gaa(C10, Y, S))
U63_gaaga(C0, D, E, C1, Y, sum_out_gaa(C10, Y, S)) → calc_out_gaaga(C0, D, E, C1, Y)
U57_aaaaaaaa(S, E, N, D, M, O, R, Y, C1, C2, calc_out_gaaga(C2, E, O, C3, N)) → U58_aaaaaaaa(S, E, N, D, M, O, R, Y, C1, calc_in_gaaga(C1, N, R, C2, E))
U58_aaaaaaaa(S, E, N, D, M, O, R, Y, C1, calc_out_gaaga(C1, N, R, C2, E)) → U59_aaaaaaaa(S, E, N, D, M, O, R, Y, calc_in_gaaga(0, D, E, C1, Y))
U59_aaaaaaaa(S, E, N, D, M, O, R, Y, calc_out_gaaga(0, D, E, C1, Y)) → money_out_aaaaaaaa(S, E, N, D, M, O, R, Y)

The argument filtering Pi contains the following mapping:
money_in_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8)  =  money_in_aaaaaaaa
U48_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U48_aaaaaaaa(x9)
carry_in_a(x1)  =  carry_in_a
carry_out_a(x1)  =  carry_out_a(x1)
U49_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)  =  U49_aaaaaaaa(x9, x10)
U50_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11)  =  U50_aaaaaaaa(x9, x10, x11)
U51_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12)  =  U51_aaaaaaaa(x9, x10, x11, x12)
U52_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13)  =  U52_aaaaaaaa(x9, x10, x11, x12, x13)
=_in_ga(x1, x2)  =  =_in_ga(x1)
=_out_ga(x1, x2)  =  =_out_ga(x2)
U53_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13)  =  U53_aaaaaaaa(x5, x9, x10, x11, x12, x13)
=\=_in_gg(x1, x2)  =  =\=_in_gg(x1, x2)
=\=_out_gg(x1, x2)  =  =\=_out_gg
0  =  0
U54_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13)  =  U54_aaaaaaaa(x5, x9, x10, x11, x12, x13)
domain_in_gg(x1, x2)  =  domain_in_gg(x1, x2)
.(x1, x2)  =  .(x2)
[]  =  []
domain_out_gg(x1, x2)  =  domain_out_gg
U65_gg(x1, x2, x3, x4)  =  U65_gg(x2, x4)
del_in_aga(x1, x2, x3)  =  del_in_aga(x2)
del_out_aga(x1, x2, x3)  =  del_out_aga(x3)
U67_aga(x1, x2, x3, x4, x5)  =  U67_aga(x5)
U66_gg(x1, x2, x3, x4)  =  U66_gg(x4)
U55_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13)  =  U55_aaaaaaaa(x5, x9, x10, x11, x12, x13)
=\=_in_ag(x1, x2)  =  =\=_in_ag(x2)
=\=_out_ag(x1, x2)  =  =\=_out_ag
U56_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12)  =  U56_aaaaaaaa(x5, x9, x10, x11, x12)
calc_in_gagga(x1, x2, x3, x4, x5)  =  calc_in_gagga(x1, x3, x4)
U60_gagga(x1, x2, x3, x4, x5, x6)  =  U60_gagga(x3, x4, x6)
sum_in_gaa(x1, x2, x3)  =  sum_in_gaa(x1)
U64_gaa(x1, x2, x3, x4)  =  U64_gaa(x4)
is_in_ag(x1, x2)  =  is_in_ag(x2)
+(x1, x2)  =  +
is_out_ag(x1, x2)  =  is_out_ag
sum_out_gaa(x1, x2, x3)  =  sum_out_gaa
U61_gagga(x1, x2, x3, x4, x5, x6)  =  U61_gagga(x4, x6)
sum_in_aga(x1, x2, x3)  =  sum_in_aga(x2)
U64_aga(x1, x2, x3, x4)  =  U64_aga(x4)
sum_out_aga(x1, x2, x3)  =  sum_out_aga
U62_gagga(x1, x2, x3, x4, x5, x6, x7)  =  U62_gagga(x7)
carry10_in_ga(x1, x2)  =  carry10_in_ga(x1)
carry10_out_ga(x1, x2)  =  carry10_out_ga(x2)
1  =  1
U63_gagga(x1, x2, x3, x4, x5, x6)  =  U63_gagga(x6)
calc_out_gagga(x1, x2, x3, x4, x5)  =  calc_out_gagga
U57_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11)  =  U57_aaaaaaaa(x5, x9, x10, x11)
calc_in_gaaga(x1, x2, x3, x4, x5)  =  calc_in_gaaga(x1, x4)
U60_gaaga(x1, x2, x3, x4, x5, x6)  =  U60_gaaga(x4, x6)
U61_gaaga(x1, x2, x3, x4, x5, x6)  =  U61_gaaga(x4, x6)
sum_in_aaa(x1, x2, x3)  =  sum_in_aaa
U64_aaa(x1, x2, x3, x4)  =  U64_aaa(x4)
sum_out_aaa(x1, x2, x3)  =  sum_out_aaa
U62_gaaga(x1, x2, x3, x4, x5, x6, x7)  =  U62_gaaga(x7)
U63_gaaga(x1, x2, x3, x4, x5, x6)  =  U63_gaaga(x6)
calc_out_gaaga(x1, x2, x3, x4, x5)  =  calc_out_gaaga
U58_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)  =  U58_aaaaaaaa(x5, x9, x10)
U59_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U59_aaaaaaaa(x5, x9)
money_out_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8)  =  money_out_aaaaaaaa(x5)
MONEY_IN_AAAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8)  =  MONEY_IN_AAAAAAAA
U48_AAAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U48_AAAAAAAA(x9)
CARRY_IN_A(x1)  =  CARRY_IN_A
U49_AAAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)  =  U49_AAAAAAAA(x9, x10)
U50_AAAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11)  =  U50_AAAAAAAA(x9, x10, x11)
U51_AAAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12)  =  U51_AAAAAAAA(x9, x10, x11, x12)
U52_AAAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13)  =  U52_AAAAAAAA(x9, x10, x11, x12, x13)
=_IN_GA(x1, x2)  =  =_IN_GA(x1)
U53_AAAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13)  =  U53_AAAAAAAA(x5, x9, x10, x11, x12, x13)
=\=_IN_GG(x1, x2)  =  =\=_IN_GG(x1, x2)
U54_AAAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13)  =  U54_AAAAAAAA(x5, x9, x10, x11, x12, x13)
DOMAIN_IN_GG(x1, x2)  =  DOMAIN_IN_GG(x1, x2)
U65_GG(x1, x2, x3, x4)  =  U65_GG(x2, x4)
DEL_IN_AGA(x1, x2, x3)  =  DEL_IN_AGA(x2)
U67_AGA(x1, x2, x3, x4, x5)  =  U67_AGA(x5)
U66_GG(x1, x2, x3, x4)  =  U66_GG(x4)
U55_AAAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13)  =  U55_AAAAAAAA(x5, x9, x10, x11, x12, x13)
=\=_IN_AG(x1, x2)  =  =\=_IN_AG(x2)
U56_AAAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12)  =  U56_AAAAAAAA(x5, x9, x10, x11, x12)
CALC_IN_GAGGA(x1, x2, x3, x4, x5)  =  CALC_IN_GAGGA(x1, x3, x4)
U60_GAGGA(x1, x2, x3, x4, x5, x6)  =  U60_GAGGA(x3, x4, x6)
SUM_IN_GAA(x1, x2, x3)  =  SUM_IN_GAA(x1)
U64_GAA(x1, x2, x3, x4)  =  U64_GAA(x4)
IS_IN_AG(x1, x2)  =  IS_IN_AG(x2)
U61_GAGGA(x1, x2, x3, x4, x5, x6)  =  U61_GAGGA(x4, x6)
SUM_IN_AGA(x1, x2, x3)  =  SUM_IN_AGA(x2)
U64_AGA(x1, x2, x3, x4)  =  U64_AGA(x4)
U62_GAGGA(x1, x2, x3, x4, x5, x6, x7)  =  U62_GAGGA(x7)
CARRY10_IN_GA(x1, x2)  =  CARRY10_IN_GA(x1)
U63_GAGGA(x1, x2, x3, x4, x5, x6)  =  U63_GAGGA(x6)
U57_AAAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11)  =  U57_AAAAAAAA(x5, x9, x10, x11)
CALC_IN_GAAGA(x1, x2, x3, x4, x5)  =  CALC_IN_GAAGA(x1, x4)
U60_GAAGA(x1, x2, x3, x4, x5, x6)  =  U60_GAAGA(x4, x6)
U61_GAAGA(x1, x2, x3, x4, x5, x6)  =  U61_GAAGA(x4, x6)
SUM_IN_AAA(x1, x2, x3)  =  SUM_IN_AAA
U64_AAA(x1, x2, x3, x4)  =  U64_AAA(x4)
U62_GAAGA(x1, x2, x3, x4, x5, x6, x7)  =  U62_GAAGA(x7)
U63_GAAGA(x1, x2, x3, x4, x5, x6)  =  U63_GAAGA(x6)
U58_AAAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)  =  U58_AAAAAAAA(x5, x9, x10)
U59_AAAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U59_AAAAAAAA(x5, x9)

We have to consider all (P,R,Pi)-chains

(9) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LOPSTR] contains 2 SCCs with 49 less nodes.

(10) Complex Obligation (AND)

(11) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

DEL_IN_AGA(X, .(Y, T), .(Y, NT)) → DEL_IN_AGA(X, T, NT)

The TRS R consists of the following rules:

money_in_aaaaaaaa(S, E, N, D, M, O, R, Y) → U48_aaaaaaaa(S, E, N, D, M, O, R, Y, carry_in_a(C1))
carry_in_a(1) → carry_out_a(1)
carry_in_a(0) → carry_out_a(0)
U48_aaaaaaaa(S, E, N, D, M, O, R, Y, carry_out_a(C1)) → U49_aaaaaaaa(S, E, N, D, M, O, R, Y, C1, carry_in_a(C2))
U49_aaaaaaaa(S, E, N, D, M, O, R, Y, C1, carry_out_a(C2)) → U50_aaaaaaaa(S, E, N, D, M, O, R, Y, C1, C2, carry_in_a(C3))
U50_aaaaaaaa(S, E, N, D, M, O, R, Y, C1, C2, carry_out_a(C3)) → U51_aaaaaaaa(S, E, N, D, M, O, R, Y, C1, C2, C3, carry_in_a(C4))
U51_aaaaaaaa(S, E, N, D, M, O, R, Y, C1, C2, C3, carry_out_a(C4)) → U52_aaaaaaaa(S, E, N, D, M, O, R, Y, C1, C2, C3, C4, =_in_ga(C4, M))
=_in_ga(X, X) → =_out_ga(X, X)
U52_aaaaaaaa(S, E, N, D, M, O, R, Y, C1, C2, C3, C4, =_out_ga(C4, M)) → U53_aaaaaaaa(S, E, N, D, M, O, R, Y, C1, C2, C3, C4, =\=_in_gg(M, 0))
=\=_in_gg(X0, X1) → =\=_out_gg(X0, X1)
U53_aaaaaaaa(S, E, N, D, M, O, R, Y, C1, C2, C3, C4, =\=_out_gg(M, 0)) → U54_aaaaaaaa(S, E, N, D, M, O, R, Y, C1, C2, C3, C4, domain_in_gg(.(S, .(E, .(N, .(D, .(M, .(O, .(R, .(Y, [])))))))), .(0, .(1, .(2, .(3, .(4, .(5, .(6, .(7, .(8, .(9, []))))))))))))
domain_in_gg([], X3) → domain_out_gg([], X3)
domain_in_gg(.(X1, R), L) → U65_gg(X1, R, L, del_in_aga(X1, L, NL))
del_in_aga(X, .(X, T), T) → del_out_aga(X, .(X, T), T)
del_in_aga(X, .(Y, T), .(Y, NT)) → U67_aga(X, Y, T, NT, del_in_aga(X, T, NT))
U67_aga(X, Y, T, NT, del_out_aga(X, T, NT)) → del_out_aga(X, .(Y, T), .(Y, NT))
U65_gg(X1, R, L, del_out_aga(X1, L, NL)) → U66_gg(X1, R, L, domain_in_gg(R, NL))
U66_gg(X1, R, L, domain_out_gg(R, NL)) → domain_out_gg(.(X1, R), L)
U54_aaaaaaaa(S, E, N, D, M, O, R, Y, C1, C2, C3, C4, domain_out_gg(.(S, .(E, .(N, .(D, .(M, .(O, .(R, .(Y, [])))))))), .(0, .(1, .(2, .(3, .(4, .(5, .(6, .(7, .(8, .(9, [])))))))))))) → U55_aaaaaaaa(S, E, N, D, M, O, R, Y, C1, C2, C3, C4, =\=_in_ag(S, 0))
=\=_in_ag(X0, X1) → =\=_out_ag(X0, X1)
U55_aaaaaaaa(S, E, N, D, M, O, R, Y, C1, C2, C3, C4, =\=_out_ag(S, 0)) → U56_aaaaaaaa(S, E, N, D, M, O, R, Y, C1, C2, C3, calc_in_gagga(C3, S, M, C4, O))
calc_in_gagga(C0, D, E, C1, Y) → U60_gagga(C0, D, E, C1, Y, sum_in_gaa(C0, D, CD))
sum_in_gaa(X, Y, Z) → U64_gaa(X, Y, Z, is_in_ag(Z, +(X, Y)))
is_in_ag(X0, X1) → is_out_ag(X0, X1)
U64_gaa(X, Y, Z, is_out_ag(Z, +(X, Y))) → sum_out_gaa(X, Y, Z)
U60_gagga(C0, D, E, C1, Y, sum_out_gaa(C0, D, CD)) → U61_gagga(C0, D, E, C1, Y, sum_in_aga(CD, E, S))
sum_in_aga(X, Y, Z) → U64_aga(X, Y, Z, is_in_ag(Z, +(X, Y)))
U64_aga(X, Y, Z, is_out_ag(Z, +(X, Y))) → sum_out_aga(X, Y, Z)
U61_gagga(C0, D, E, C1, Y, sum_out_aga(CD, E, S)) → U62_gagga(C0, D, E, C1, Y, S, carry10_in_ga(C1, C10))
carry10_in_ga(0, 0) → carry10_out_ga(0, 0)
carry10_in_ga(1, 10) → carry10_out_ga(1, 10)
U62_gagga(C0, D, E, C1, Y, S, carry10_out_ga(C1, C10)) → U63_gagga(C0, D, E, C1, Y, sum_in_gaa(C10, Y, S))
U63_gagga(C0, D, E, C1, Y, sum_out_gaa(C10, Y, S)) → calc_out_gagga(C0, D, E, C1, Y)
U56_aaaaaaaa(S, E, N, D, M, O, R, Y, C1, C2, C3, calc_out_gagga(C3, S, M, C4, O)) → U57_aaaaaaaa(S, E, N, D, M, O, R, Y, C1, C2, calc_in_gaaga(C2, E, O, C3, N))
calc_in_gaaga(C0, D, E, C1, Y) → U60_gaaga(C0, D, E, C1, Y, sum_in_gaa(C0, D, CD))
U60_gaaga(C0, D, E, C1, Y, sum_out_gaa(C0, D, CD)) → U61_gaaga(C0, D, E, C1, Y, sum_in_aaa(CD, E, S))
sum_in_aaa(X, Y, Z) → U64_aaa(X, Y, Z, is_in_ag(Z, +(X, Y)))
U64_aaa(X, Y, Z, is_out_ag(Z, +(X, Y))) → sum_out_aaa(X, Y, Z)
U61_gaaga(C0, D, E, C1, Y, sum_out_aaa(CD, E, S)) → U62_gaaga(C0, D, E, C1, Y, S, carry10_in_ga(C1, C10))
U62_gaaga(C0, D, E, C1, Y, S, carry10_out_ga(C1, C10)) → U63_gaaga(C0, D, E, C1, Y, sum_in_gaa(C10, Y, S))
U63_gaaga(C0, D, E, C1, Y, sum_out_gaa(C10, Y, S)) → calc_out_gaaga(C0, D, E, C1, Y)
U57_aaaaaaaa(S, E, N, D, M, O, R, Y, C1, C2, calc_out_gaaga(C2, E, O, C3, N)) → U58_aaaaaaaa(S, E, N, D, M, O, R, Y, C1, calc_in_gaaga(C1, N, R, C2, E))
U58_aaaaaaaa(S, E, N, D, M, O, R, Y, C1, calc_out_gaaga(C1, N, R, C2, E)) → U59_aaaaaaaa(S, E, N, D, M, O, R, Y, calc_in_gaaga(0, D, E, C1, Y))
U59_aaaaaaaa(S, E, N, D, M, O, R, Y, calc_out_gaaga(0, D, E, C1, Y)) → money_out_aaaaaaaa(S, E, N, D, M, O, R, Y)

The argument filtering Pi contains the following mapping:
money_in_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8)  =  money_in_aaaaaaaa
U48_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U48_aaaaaaaa(x9)
carry_in_a(x1)  =  carry_in_a
carry_out_a(x1)  =  carry_out_a(x1)
U49_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)  =  U49_aaaaaaaa(x9, x10)
U50_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11)  =  U50_aaaaaaaa(x9, x10, x11)
U51_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12)  =  U51_aaaaaaaa(x9, x10, x11, x12)
U52_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13)  =  U52_aaaaaaaa(x9, x10, x11, x12, x13)
=_in_ga(x1, x2)  =  =_in_ga(x1)
=_out_ga(x1, x2)  =  =_out_ga(x2)
U53_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13)  =  U53_aaaaaaaa(x5, x9, x10, x11, x12, x13)
=\=_in_gg(x1, x2)  =  =\=_in_gg(x1, x2)
=\=_out_gg(x1, x2)  =  =\=_out_gg
0  =  0
U54_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13)  =  U54_aaaaaaaa(x5, x9, x10, x11, x12, x13)
domain_in_gg(x1, x2)  =  domain_in_gg(x1, x2)
.(x1, x2)  =  .(x2)
[]  =  []
domain_out_gg(x1, x2)  =  domain_out_gg
U65_gg(x1, x2, x3, x4)  =  U65_gg(x2, x4)
del_in_aga(x1, x2, x3)  =  del_in_aga(x2)
del_out_aga(x1, x2, x3)  =  del_out_aga(x3)
U67_aga(x1, x2, x3, x4, x5)  =  U67_aga(x5)
U66_gg(x1, x2, x3, x4)  =  U66_gg(x4)
U55_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13)  =  U55_aaaaaaaa(x5, x9, x10, x11, x12, x13)
=\=_in_ag(x1, x2)  =  =\=_in_ag(x2)
=\=_out_ag(x1, x2)  =  =\=_out_ag
U56_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12)  =  U56_aaaaaaaa(x5, x9, x10, x11, x12)
calc_in_gagga(x1, x2, x3, x4, x5)  =  calc_in_gagga(x1, x3, x4)
U60_gagga(x1, x2, x3, x4, x5, x6)  =  U60_gagga(x3, x4, x6)
sum_in_gaa(x1, x2, x3)  =  sum_in_gaa(x1)
U64_gaa(x1, x2, x3, x4)  =  U64_gaa(x4)
is_in_ag(x1, x2)  =  is_in_ag(x2)
+(x1, x2)  =  +
is_out_ag(x1, x2)  =  is_out_ag
sum_out_gaa(x1, x2, x3)  =  sum_out_gaa
U61_gagga(x1, x2, x3, x4, x5, x6)  =  U61_gagga(x4, x6)
sum_in_aga(x1, x2, x3)  =  sum_in_aga(x2)
U64_aga(x1, x2, x3, x4)  =  U64_aga(x4)
sum_out_aga(x1, x2, x3)  =  sum_out_aga
U62_gagga(x1, x2, x3, x4, x5, x6, x7)  =  U62_gagga(x7)
carry10_in_ga(x1, x2)  =  carry10_in_ga(x1)
carry10_out_ga(x1, x2)  =  carry10_out_ga(x2)
1  =  1
U63_gagga(x1, x2, x3, x4, x5, x6)  =  U63_gagga(x6)
calc_out_gagga(x1, x2, x3, x4, x5)  =  calc_out_gagga
U57_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11)  =  U57_aaaaaaaa(x5, x9, x10, x11)
calc_in_gaaga(x1, x2, x3, x4, x5)  =  calc_in_gaaga(x1, x4)
U60_gaaga(x1, x2, x3, x4, x5, x6)  =  U60_gaaga(x4, x6)
U61_gaaga(x1, x2, x3, x4, x5, x6)  =  U61_gaaga(x4, x6)
sum_in_aaa(x1, x2, x3)  =  sum_in_aaa
U64_aaa(x1, x2, x3, x4)  =  U64_aaa(x4)
sum_out_aaa(x1, x2, x3)  =  sum_out_aaa
U62_gaaga(x1, x2, x3, x4, x5, x6, x7)  =  U62_gaaga(x7)
U63_gaaga(x1, x2, x3, x4, x5, x6)  =  U63_gaaga(x6)
calc_out_gaaga(x1, x2, x3, x4, x5)  =  calc_out_gaaga
U58_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)  =  U58_aaaaaaaa(x5, x9, x10)
U59_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U59_aaaaaaaa(x5, x9)
money_out_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8)  =  money_out_aaaaaaaa(x5)
DEL_IN_AGA(x1, x2, x3)  =  DEL_IN_AGA(x2)

We have to consider all (P,R,Pi)-chains

(12) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(13) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

DEL_IN_AGA(X, .(Y, T), .(Y, NT)) → DEL_IN_AGA(X, T, NT)

R is empty.
The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x2)
DEL_IN_AGA(x1, x2, x3)  =  DEL_IN_AGA(x2)

We have to consider all (P,R,Pi)-chains

(14) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(15) Obligation:

Q DP problem:
The TRS P consists of the following rules:

DEL_IN_AGA(.(T)) → DEL_IN_AGA(T)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(16) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

  • DEL_IN_AGA(.(T)) → DEL_IN_AGA(T)
    The graph contains the following edges 1 > 1

(17) YES

(18) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

U65_GG(X1, R, L, del_out_aga(X1, L, NL)) → DOMAIN_IN_GG(R, NL)
DOMAIN_IN_GG(.(X1, R), L) → U65_GG(X1, R, L, del_in_aga(X1, L, NL))

The TRS R consists of the following rules:

money_in_aaaaaaaa(S, E, N, D, M, O, R, Y) → U48_aaaaaaaa(S, E, N, D, M, O, R, Y, carry_in_a(C1))
carry_in_a(1) → carry_out_a(1)
carry_in_a(0) → carry_out_a(0)
U48_aaaaaaaa(S, E, N, D, M, O, R, Y, carry_out_a(C1)) → U49_aaaaaaaa(S, E, N, D, M, O, R, Y, C1, carry_in_a(C2))
U49_aaaaaaaa(S, E, N, D, M, O, R, Y, C1, carry_out_a(C2)) → U50_aaaaaaaa(S, E, N, D, M, O, R, Y, C1, C2, carry_in_a(C3))
U50_aaaaaaaa(S, E, N, D, M, O, R, Y, C1, C2, carry_out_a(C3)) → U51_aaaaaaaa(S, E, N, D, M, O, R, Y, C1, C2, C3, carry_in_a(C4))
U51_aaaaaaaa(S, E, N, D, M, O, R, Y, C1, C2, C3, carry_out_a(C4)) → U52_aaaaaaaa(S, E, N, D, M, O, R, Y, C1, C2, C3, C4, =_in_ga(C4, M))
=_in_ga(X, X) → =_out_ga(X, X)
U52_aaaaaaaa(S, E, N, D, M, O, R, Y, C1, C2, C3, C4, =_out_ga(C4, M)) → U53_aaaaaaaa(S, E, N, D, M, O, R, Y, C1, C2, C3, C4, =\=_in_gg(M, 0))
=\=_in_gg(X0, X1) → =\=_out_gg(X0, X1)
U53_aaaaaaaa(S, E, N, D, M, O, R, Y, C1, C2, C3, C4, =\=_out_gg(M, 0)) → U54_aaaaaaaa(S, E, N, D, M, O, R, Y, C1, C2, C3, C4, domain_in_gg(.(S, .(E, .(N, .(D, .(M, .(O, .(R, .(Y, [])))))))), .(0, .(1, .(2, .(3, .(4, .(5, .(6, .(7, .(8, .(9, []))))))))))))
domain_in_gg([], X3) → domain_out_gg([], X3)
domain_in_gg(.(X1, R), L) → U65_gg(X1, R, L, del_in_aga(X1, L, NL))
del_in_aga(X, .(X, T), T) → del_out_aga(X, .(X, T), T)
del_in_aga(X, .(Y, T), .(Y, NT)) → U67_aga(X, Y, T, NT, del_in_aga(X, T, NT))
U67_aga(X, Y, T, NT, del_out_aga(X, T, NT)) → del_out_aga(X, .(Y, T), .(Y, NT))
U65_gg(X1, R, L, del_out_aga(X1, L, NL)) → U66_gg(X1, R, L, domain_in_gg(R, NL))
U66_gg(X1, R, L, domain_out_gg(R, NL)) → domain_out_gg(.(X1, R), L)
U54_aaaaaaaa(S, E, N, D, M, O, R, Y, C1, C2, C3, C4, domain_out_gg(.(S, .(E, .(N, .(D, .(M, .(O, .(R, .(Y, [])))))))), .(0, .(1, .(2, .(3, .(4, .(5, .(6, .(7, .(8, .(9, [])))))))))))) → U55_aaaaaaaa(S, E, N, D, M, O, R, Y, C1, C2, C3, C4, =\=_in_ag(S, 0))
=\=_in_ag(X0, X1) → =\=_out_ag(X0, X1)
U55_aaaaaaaa(S, E, N, D, M, O, R, Y, C1, C2, C3, C4, =\=_out_ag(S, 0)) → U56_aaaaaaaa(S, E, N, D, M, O, R, Y, C1, C2, C3, calc_in_gagga(C3, S, M, C4, O))
calc_in_gagga(C0, D, E, C1, Y) → U60_gagga(C0, D, E, C1, Y, sum_in_gaa(C0, D, CD))
sum_in_gaa(X, Y, Z) → U64_gaa(X, Y, Z, is_in_ag(Z, +(X, Y)))
is_in_ag(X0, X1) → is_out_ag(X0, X1)
U64_gaa(X, Y, Z, is_out_ag(Z, +(X, Y))) → sum_out_gaa(X, Y, Z)
U60_gagga(C0, D, E, C1, Y, sum_out_gaa(C0, D, CD)) → U61_gagga(C0, D, E, C1, Y, sum_in_aga(CD, E, S))
sum_in_aga(X, Y, Z) → U64_aga(X, Y, Z, is_in_ag(Z, +(X, Y)))
U64_aga(X, Y, Z, is_out_ag(Z, +(X, Y))) → sum_out_aga(X, Y, Z)
U61_gagga(C0, D, E, C1, Y, sum_out_aga(CD, E, S)) → U62_gagga(C0, D, E, C1, Y, S, carry10_in_ga(C1, C10))
carry10_in_ga(0, 0) → carry10_out_ga(0, 0)
carry10_in_ga(1, 10) → carry10_out_ga(1, 10)
U62_gagga(C0, D, E, C1, Y, S, carry10_out_ga(C1, C10)) → U63_gagga(C0, D, E, C1, Y, sum_in_gaa(C10, Y, S))
U63_gagga(C0, D, E, C1, Y, sum_out_gaa(C10, Y, S)) → calc_out_gagga(C0, D, E, C1, Y)
U56_aaaaaaaa(S, E, N, D, M, O, R, Y, C1, C2, C3, calc_out_gagga(C3, S, M, C4, O)) → U57_aaaaaaaa(S, E, N, D, M, O, R, Y, C1, C2, calc_in_gaaga(C2, E, O, C3, N))
calc_in_gaaga(C0, D, E, C1, Y) → U60_gaaga(C0, D, E, C1, Y, sum_in_gaa(C0, D, CD))
U60_gaaga(C0, D, E, C1, Y, sum_out_gaa(C0, D, CD)) → U61_gaaga(C0, D, E, C1, Y, sum_in_aaa(CD, E, S))
sum_in_aaa(X, Y, Z) → U64_aaa(X, Y, Z, is_in_ag(Z, +(X, Y)))
U64_aaa(X, Y, Z, is_out_ag(Z, +(X, Y))) → sum_out_aaa(X, Y, Z)
U61_gaaga(C0, D, E, C1, Y, sum_out_aaa(CD, E, S)) → U62_gaaga(C0, D, E, C1, Y, S, carry10_in_ga(C1, C10))
U62_gaaga(C0, D, E, C1, Y, S, carry10_out_ga(C1, C10)) → U63_gaaga(C0, D, E, C1, Y, sum_in_gaa(C10, Y, S))
U63_gaaga(C0, D, E, C1, Y, sum_out_gaa(C10, Y, S)) → calc_out_gaaga(C0, D, E, C1, Y)
U57_aaaaaaaa(S, E, N, D, M, O, R, Y, C1, C2, calc_out_gaaga(C2, E, O, C3, N)) → U58_aaaaaaaa(S, E, N, D, M, O, R, Y, C1, calc_in_gaaga(C1, N, R, C2, E))
U58_aaaaaaaa(S, E, N, D, M, O, R, Y, C1, calc_out_gaaga(C1, N, R, C2, E)) → U59_aaaaaaaa(S, E, N, D, M, O, R, Y, calc_in_gaaga(0, D, E, C1, Y))
U59_aaaaaaaa(S, E, N, D, M, O, R, Y, calc_out_gaaga(0, D, E, C1, Y)) → money_out_aaaaaaaa(S, E, N, D, M, O, R, Y)

The argument filtering Pi contains the following mapping:
money_in_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8)  =  money_in_aaaaaaaa
U48_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U48_aaaaaaaa(x9)
carry_in_a(x1)  =  carry_in_a
carry_out_a(x1)  =  carry_out_a(x1)
U49_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)  =  U49_aaaaaaaa(x9, x10)
U50_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11)  =  U50_aaaaaaaa(x9, x10, x11)
U51_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12)  =  U51_aaaaaaaa(x9, x10, x11, x12)
U52_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13)  =  U52_aaaaaaaa(x9, x10, x11, x12, x13)
=_in_ga(x1, x2)  =  =_in_ga(x1)
=_out_ga(x1, x2)  =  =_out_ga(x2)
U53_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13)  =  U53_aaaaaaaa(x5, x9, x10, x11, x12, x13)
=\=_in_gg(x1, x2)  =  =\=_in_gg(x1, x2)
=\=_out_gg(x1, x2)  =  =\=_out_gg
0  =  0
U54_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13)  =  U54_aaaaaaaa(x5, x9, x10, x11, x12, x13)
domain_in_gg(x1, x2)  =  domain_in_gg(x1, x2)
.(x1, x2)  =  .(x2)
[]  =  []
domain_out_gg(x1, x2)  =  domain_out_gg
U65_gg(x1, x2, x3, x4)  =  U65_gg(x2, x4)
del_in_aga(x1, x2, x3)  =  del_in_aga(x2)
del_out_aga(x1, x2, x3)  =  del_out_aga(x3)
U67_aga(x1, x2, x3, x4, x5)  =  U67_aga(x5)
U66_gg(x1, x2, x3, x4)  =  U66_gg(x4)
U55_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13)  =  U55_aaaaaaaa(x5, x9, x10, x11, x12, x13)
=\=_in_ag(x1, x2)  =  =\=_in_ag(x2)
=\=_out_ag(x1, x2)  =  =\=_out_ag
U56_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12)  =  U56_aaaaaaaa(x5, x9, x10, x11, x12)
calc_in_gagga(x1, x2, x3, x4, x5)  =  calc_in_gagga(x1, x3, x4)
U60_gagga(x1, x2, x3, x4, x5, x6)  =  U60_gagga(x3, x4, x6)
sum_in_gaa(x1, x2, x3)  =  sum_in_gaa(x1)
U64_gaa(x1, x2, x3, x4)  =  U64_gaa(x4)
is_in_ag(x1, x2)  =  is_in_ag(x2)
+(x1, x2)  =  +
is_out_ag(x1, x2)  =  is_out_ag
sum_out_gaa(x1, x2, x3)  =  sum_out_gaa
U61_gagga(x1, x2, x3, x4, x5, x6)  =  U61_gagga(x4, x6)
sum_in_aga(x1, x2, x3)  =  sum_in_aga(x2)
U64_aga(x1, x2, x3, x4)  =  U64_aga(x4)
sum_out_aga(x1, x2, x3)  =  sum_out_aga
U62_gagga(x1, x2, x3, x4, x5, x6, x7)  =  U62_gagga(x7)
carry10_in_ga(x1, x2)  =  carry10_in_ga(x1)
carry10_out_ga(x1, x2)  =  carry10_out_ga(x2)
1  =  1
U63_gagga(x1, x2, x3, x4, x5, x6)  =  U63_gagga(x6)
calc_out_gagga(x1, x2, x3, x4, x5)  =  calc_out_gagga
U57_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11)  =  U57_aaaaaaaa(x5, x9, x10, x11)
calc_in_gaaga(x1, x2, x3, x4, x5)  =  calc_in_gaaga(x1, x4)
U60_gaaga(x1, x2, x3, x4, x5, x6)  =  U60_gaaga(x4, x6)
U61_gaaga(x1, x2, x3, x4, x5, x6)  =  U61_gaaga(x4, x6)
sum_in_aaa(x1, x2, x3)  =  sum_in_aaa
U64_aaa(x1, x2, x3, x4)  =  U64_aaa(x4)
sum_out_aaa(x1, x2, x3)  =  sum_out_aaa
U62_gaaga(x1, x2, x3, x4, x5, x6, x7)  =  U62_gaaga(x7)
U63_gaaga(x1, x2, x3, x4, x5, x6)  =  U63_gaaga(x6)
calc_out_gaaga(x1, x2, x3, x4, x5)  =  calc_out_gaaga
U58_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)  =  U58_aaaaaaaa(x5, x9, x10)
U59_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U59_aaaaaaaa(x5, x9)
money_out_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8)  =  money_out_aaaaaaaa(x5)
DOMAIN_IN_GG(x1, x2)  =  DOMAIN_IN_GG(x1, x2)
U65_GG(x1, x2, x3, x4)  =  U65_GG(x2, x4)

We have to consider all (P,R,Pi)-chains

(19) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(20) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

U65_GG(X1, R, L, del_out_aga(X1, L, NL)) → DOMAIN_IN_GG(R, NL)
DOMAIN_IN_GG(.(X1, R), L) → U65_GG(X1, R, L, del_in_aga(X1, L, NL))

The TRS R consists of the following rules:

del_in_aga(X, .(X, T), T) → del_out_aga(X, .(X, T), T)
del_in_aga(X, .(Y, T), .(Y, NT)) → U67_aga(X, Y, T, NT, del_in_aga(X, T, NT))
U67_aga(X, Y, T, NT, del_out_aga(X, T, NT)) → del_out_aga(X, .(Y, T), .(Y, NT))

The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x2)
del_in_aga(x1, x2, x3)  =  del_in_aga(x2)
del_out_aga(x1, x2, x3)  =  del_out_aga(x3)
U67_aga(x1, x2, x3, x4, x5)  =  U67_aga(x5)
DOMAIN_IN_GG(x1, x2)  =  DOMAIN_IN_GG(x1, x2)
U65_GG(x1, x2, x3, x4)  =  U65_GG(x2, x4)

We have to consider all (P,R,Pi)-chains

(21) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(22) Obligation:

Q DP problem:
The TRS P consists of the following rules:

U65_GG(R, del_out_aga(NL)) → DOMAIN_IN_GG(R, NL)
DOMAIN_IN_GG(.(R), L) → U65_GG(R, del_in_aga(L))

The TRS R consists of the following rules:

del_in_aga(.(T)) → del_out_aga(T)
del_in_aga(.(T)) → U67_aga(del_in_aga(T))
U67_aga(del_out_aga(NT)) → del_out_aga(.(NT))

The set Q consists of the following terms:

del_in_aga(x0)
U67_aga(x0)

We have to consider all (P,Q,R)-chains.

(23) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

  • DOMAIN_IN_GG(.(R), L) → U65_GG(R, del_in_aga(L))
    The graph contains the following edges 1 > 1

  • U65_GG(R, del_out_aga(NL)) → DOMAIN_IN_GG(R, NL)
    The graph contains the following edges 1 >= 1, 2 > 2

(24) YES